Cousin Marie : Formalisation du théorème de décomposition de Hahn avec le démonstrateur interactif Isabelle

De Ensiwiki
Aller à : navigation, rechercher
Cornues.png
Titre du projet Formalisation du théorème de décomposition de Hahn avec le démonstrateur interactif Isabelle
Cadre IRL

Labo LIG
Équipe CAPP
Encadrants Mnacho Echenim et Hervé Guiol


Introduction

Dans le cadre de l'IRL, j'ai formalisé en Isabelle le théorème de décomposition de Hahn et le théorème de décomposition de Jordan. Ces deux théorèmes sont des résultats importants de la théorie de la mesure.

Les assistants de preuve sont des logiciels à l'aide desquels on peut formaliser une preuve ou un raisonnement mathématique. Lors de la formalisation dans un assistant de preuve, chaque étape de la preuve est vérifiée, comme la preuve elle-même dans sa globalité. Ils permettent donc d'assurer qu'une preuve mathématique est correcte.

De plus en plus de résultats mathématiques sont formalisées dans ces assistants de preuve, et formaliser ces résultats est un domaine de recherche qui occupe et intéresse de plus en plus de mathématiciens et informaticiens.

Ces logiciels utilisent par ailleurs des langages hybrides, proches des langages de programmation et du langage naturel mathématique, afin d'être compris des mathématiciens et des machines, même si une preuve formalisée est parfois très peu intuitive car trop détaillée (et donc très rapidement très longue) pour un être humain.

J'ai ici travaillé avec le logiciel Isabelle HOL, qui est un démonstrateur interactif basé sur la logique d'ordre supérieur, développé en partenariat par les universités de Cambridge et Munich [1], dont la première version a été publiée en 1986.

Motivation

Le but de formaliser ces deux théorèmes est de manipuler et formaliser en Isabelle la notion de mesure signée, manipuler des mesures et des ensembles, pour finalement aboutir à la preuve de théorèmes importants de la théorie de la mesure. De plus, ce projet a pour but de me faire manipuler Isabelle, et découvrir le domaine des assistants de preuves.

Le théorème de Hahn demande de généraliser la notion de mesure standard pour aboutir à la notion de mesure signée, et celui de Jordan permet de faire le lien entre ces deux notions de mesure. Il y a donc un lien très fort entre ces théorèmes et la théorie de la mesure.

Ces résultats, une fois formalisé en Isabelle, pourront être utilisé par d'autres mathématiciens, pour prouver d'autres résultats de la théorie de la mesure, comme par exemple une extension du théorème de Radon-Nikodým aux mesures signées. En effet, en Isabelle, un fichier est appelé une théorie (extension .thy), et tous les résultats formalisés et publiés [4] peuvent être disponibles si on les importe dans une théorie.

Quelques notions

Afin de pouvoir mieux appréhender le théorème de décomposition de Hahn, nous posons quelques définitions:

La notion de mesure signée est proche de la notion standard de mesure, sauf que dans le cas d'une mesure signée, l'image des ensembles mesurables peut être positive ou négative. Une mesure signée [2] \mu associée à un espace mesurable {X, \mathcal{A}} est une application de \mathcal{A} dans les réels étendus, et telle que :

  • la mesure de l'ensemble vide est nulle
  • elle ne peut contenir à la fois +\infty et -\infty dans son ensemble image
  • \mu est \sigma-additive.

Nous nous plaçons dorénavant dans l'espace mesurable {X, \mathcal{A}} avec la mesure signée \mu.

Un ensemble E est positif [2] (resp. négatif) si :

  • E est mesurable (i.e. E \in \mathcal{A})
  • pour tout sous ensemble A mesurable de E, on a : \mu(A) \geq 0 (resp. \mu(A) \leq 0).

Théorème de décomposition de Hahn

Le théorème de décomposition de Hahn [2] est le suivant : soit { X , \mathcal{A}} un espace mesurable et \mu une mesure signée sur {X, \mathcal{A}}. Alors il existe une partition de  X en P un ensemble positif et  N un ensemble négatif. Cette partition est unique à tout ensemble de mesure \mu nulle près.

C'est ce théorème que j'ai formalisé en Isabelle dans un premier temps. J'ai ensuite formalisé le théorème de décomposition de Jordan, qui est une conséquence du théorème de décomposition de Jordan.

Théorème de décomposition de Jordan

Le théorème de Jordan est le suivant [3] : Soit {X, \mathcal{A}} un espace mesurable. Toute mesure \mu sur \mathcal{A} possède une unique décomposition de la forme \mu = m - n, où m et n sont deux mesures positives, dont au moins l'une est finie, et telles que :

  • m(E) = 0 pour tout E mesurable tel que E est un sous-ensemble de N
  • n(E) = 0 pour tout E mesurable tel que E est un sous-ensemble de P

P et N sont les deux ensembles respectivement positifs et négatifs de la décomposition de Hahn, i.e. tels que X = P \cup N.

Formalisation

Pour formaliser ces théorèmes en Isabelle, leurs preuves et les notions qui y sont associées, il a d'abord fallu détailler la preuve mathématique.

En effet, j'ai détaillé mathématiquement la preuve de chacun des théorème (ce qui revient à les découper en petites étapes), afin de pouvoir indiquer les mécanismes mis en jeu, et afin de bien comprendre les preuves.

Une fois ce travail fait, j'ai formalisé cette preuve détaillé dans Isabelle, où j'ai du détailler encore plus les raisonnements (pour donner une petite idée, le fichier en Isabelle fait 900 lignes ; il a fallu introduire des définitions et lemmes préliminaires aux théorèmes, les prouver, puis formaliser les preuves des résultats en Isabelle).

Pour plus de détail sur la formalisation, vous pouvez la trouver sur le dépôt git suivant : https://gitlab.ensimag.fr/cousinm/irl-hahndecompositionthm, dans le fichier "HahnDecomp.thy".

Résultats obtenus

Les deux théorèmes sont maintenant formalisés dans Isabelle, même si il m'a fallu du temps pour bien comprendre les théorèmes, et encore plus de temps pour apprivoiser Isabelle. De plus, la formalisation de ces théorèmes a nécessité la formalisation d'autres lemmes et propositions intermédiaire, qui est finie pour la plupart d'entre eux mais encore en cours pour certains.

Bilan

Ce projet d'IRL a été très intéressant de par plusieurs aspects :

  • il m'a permis d'une part de découvrir le monde du travail en laboratoire
  • j'ai de plus manipulé des notions de la théorie de la mesure, de manière plus poussée que ce que l'on a vu en cours
  • j'ai découvert les assistants de preuves et plus particulièrement Isabelle
  • j'ai compris (et expérimenté) ce que voulait vraiment dire formaliser un raisonnement.

Aussi, ce projet a été très riche et m'a énormément plu, j'aurais aimé qu'il dure plus longtemps ! Il a confirmé mon envie de faire mon PFE dans un laboratoire de recherche, et de poursuivre mes études en faisant une thèse.

Pour plus de détail sur ce que j'ai fait (et comment je l'ai fait), je vous invite à lire mon rapport, disponible dans la section éponyme.

Remerciements

Je voudrais adresser un énorme merci à Mnacho Echenim et Hervé Guiol pour leur accompagnement extraordinaire et leurs explications tout au long de ce projet.

Rapport

Rapport : Fichier:Rapport cousin marie.pdf

Références

[1] https://isabelle.in.tum.de/overview.html

[2] Emmanuele DiBenedetto, "Real Analysis", Birkhäuser Advanced Texts Basler Lehrbücher, 2016

[3] https://en.wikipedia.org/wiki/Hahn_decomposition_theorem

[4] Archive des preuves formelles, https://www.isa-afp.org/