The continuous functional calculus in Lean

Résumé Technique : Le Calcul Fonctionnel Continu dans Lean

Énoncé du Problème
Le calcul fonctionnel continu est un outil fondamental dans la théorie des $C^*$-algèbres, permettant d'identifier les sous-algèbres $C^*$ commutatives avec les algèbres de fonctions continues sur des espaces compacts de Hausdorff. Bien que mathématiquement bien compris, sa formalisation dans des assistants de preuve comme Lean présente des défis significatifs. La difficulté principale réside dans l'équilibre entre la fidélité mathématique et l'utilisabilité. Une définition mathématique « naturelle » repose souvent sur des types dépendants (par exemple, des fonctions définies uniquement sur le spectre d'un élément) et des structures groupées (par exemple, des applications continues comme un type spécifique). Bien que ces approches soient rigoureuses, elles créent des frictions dans les preuves formelles : réécrire des égalités devient difficile car les types dépendent d'éléments spécifiques, et composer des fonctions nécessite de gérer des coercitions de sous-types complexes et des preuves de continuité. Les auteurs ont identifié qu'une conception privilégiant la simplicité mathématique stricte échoue aux « tests de l'étalon » de l'utilisabilité pratique requis pour une bibliothèque comme Mathlib.

Méthodologie et Décisions de Conception
Les auteurs ont développé une formalisation du calcul fonctionnel continu dans Lean 4, intégrée à la bibliothèque Mathlib. Leur méthodologie a impliqué un processus de conception itératif, passant d'une définition mathématiquement « pure » à une interface « utilitaire ». Les décisions de conception clés incluent :

1. Dégroupage et « Valeurs de Déchet » (Junk Values) :
   Au lieu de définir le calcul fonctionnel comme une application de le type des fonctions continues sur le spectre $C(\sigma(a), \mathbb{C})$ vers l'algèbre, les auteurs ont défini une fonction cfc qui accepte n'importe quelle fonction $f: \mathbb{C} \to \mathbb{C}$ et n'importe quel élément $a$. Si $a$ n'est pas normal ou si $f$ n'est pas continue sur le spectre, la fonction retourne une « valeur de déchet » (typiquement 0).

   • Raisonnement : Cela permet aux utilisateurs d'écrire des expressions comme $f(a)$ sans avoir à prouver d'abord que $a$ est normale ou que $f$ est continue. Cela imite l'approche « écrire d'abord, réfléchir plus tard » des mathématiques informelles, retardant la charge de la preuve jusqu'à ce qu'une propriété non triviale soit nécessaire. Cela permet également une réécriture (rw) fluide car les types des arguments ne dépendent plus des propriétés spécifiques de $a$.

2. Abstraction par Classe :
   Pour gérer différents anneaux scalaires ($\mathbb{C}$, $\mathbb{R}$, et $\mathbb{R}_{\ge 0}$) et différents types d'éléments (normaux, auto-adjoints, non-négatifs), les auteurs ont implémenté le calcul comme une classe de type ContinuousFunctionalCalculus.

   • Généralisation de Prédicat : La classe est paramétrée par un prédicat $p$ sur les éléments de l'algèbre (par exemple, IsStarNormal, IsSelfAdjoint, 0 ≤ a). Cela permet à une interface unique de couvrir divers cas sans duplication de code.
   • Prop ou Donnée : Les versions antérieures incluaient l'isomorphisme $*$-en tant que donnée. Cependant, pour éviter les problèmes d'égalité définitionnelle (où deux constructions différentes de la même application pourraient ne pas être définitionnellement égales), la conception finale fait de la classe un Prop. Elle affirme l'existence d'un unique $*$-isomorphisme possédant des propriétés spécifiques, plutôt que de stocker l'application elle-même.

3. Gestion des Algèbres Non-Unitaires :
   La formalisation s'étend aux $C^*$-algèbres non unitaires. Au lieu de s'appuyer sur des constructions extrinsèques comme l'unitisation minimale pour chaque définition, les auteurs ont introduit une définition intrinsèque du quasispectre. Le calcul fonctionnel non unitaire est défini sur les fonctions s'annulant en 0 (ou envoyant 0 sur 0), évitant ainsi de devoir constamment basculer entre les contextes unitaires et non unitaires.

4. Automatisation via autoParam :
   Pour atténuer la verbosité du passage manuel des preuves de continuité et de normalité, les auteurs ont utilisé la fonctionnalité autoParam de Lean. Les hypothèses telles que « $f$ est continue sur le spectre » sont équipées de tactiques par défaut. Si l'utilisateur ne fournit pas de preuve, Lean tente de la synthétiser automatiquement en utilisant des lemmes existants (par exemple, aesop, fun_prop).

5. L'Unicité comme une Classe Séparée :
   La propriété de composition ($g(f(a)) = (g \circ f)(a)$) est centrale à la théorie. Les auteurs ont prouvé cela en utilisant un argument d'unicité plutôt que le théorème de Stone–Weierstrass (qui échoue pour $\mathbb{R}_{\ge 0}$). Ils ont encapsulé l'unicité des $*$-isomorphismes dans une classe séparée ContinuousMap.UniqueHom, permettant à la propriété de composition d'être dérivée génériquement à travers différents anneaux scalaires.

Contributions Clés et Résultats

• Première Formalisation : Ce travail constitue la première formalisation du calcul fonctionnel continu dans n'importe quel assistant de preuve.
• Intégration à Mathlib : L'implémentation est fusionnée dans Mathlib, fournissant une interface unifiée pour les calculs fonctionnels complexes, réels et de réels non-négatifs.
• Vérification de l'Usabilité : La conception a été validée par des « tests de l'étalon » spécifiques, incluant :
  • La définition d'inverses ($f(a^{-1})$) en utilisant des fonctions non continues partout (par exemple, $x \mapsto x^{-1}$).
  • La construction de parties positives/négatives et de racines carrées pour des éléments auto-adjoints et non-négatifs.
  • L'application du calcul à des matrices sur $\mathbb{R}$ (qui ne possèdent pas de structure métrique globale dans Mathlib).
• Automatisation : L'interface supporte une automatisation de haut niveau, permettant aux utilisateurs de prouver des propriétés comme $f(-a) = (x \mapsto f(-x))(a)$ avec une intervention manuelle minimale.
• Applications : L'interface a déjà été utilisée pour formaliser des résultats avancés, notamment :
  • L'existence d'unités approximatives dans les $C^*$-algèbres non unitaires.
  • La continuité du calcul fonctionnel dans les deux variables.
  • Les propriétés des applications $a \mapsto |a|$, $a \mapsto a^p$, et $a \mapsto \log(a)$.
  • Des résultats concernant les éléments unitaires et les projections.

Signification et Limites
Le papier revendique sa signification principalement dans sa philosophie de conception : démontrer que pour qu'un outil soit efficace dans une grande bibliothèque formelle, il doit prioriser l'ergonomie de l'utilisateur final (l'usabilité) sur la pureté mathématique stricte de la définition. En acceptant des « valeurs de déchet » et en dégroupant les types, les auteurs ont créé une interface qui se comporte intuitivement pour les mathématiciens, permettant des manipulations complexes (comme la composition et la réécriture) qui seraient prohibitivement difficiles avec une approche de type strictement dépendant.

Les auteurs font preuve de modestie quant à l'état actuel, reconnaissant plusieurs limites :

• Lemmes simp : En raison de la nécessité d'arguments explicites pour déclencher autoParam, de nombreux lemmes ne peuvent pas être utilisés comme règles simp sans intervention manuelle, rendant certaines preuves plus verbeuses que souhaité.
• Complications de $\mathbb{R}_{\ge 0}$ : L'utilisation des réels non-négatifs comme anneau scalaire introduit des obstacles techniques spécifiques (par exemple, la soustraction tronquée, l'absence de structure d'anneau) qui nécessitent des énoncés de théorèmes distincts.
• $C^*$-algèbres réelles : Bien que le cadre soit conçu pour supporter les $C^*$-algèbres réelles, le cas spécifique du calcul fonctionnel sur $\mathbb{C}$ pour les algèbres réelles (qui nécessite un domaine de fonctions différent) n'est pas encore pleinement intégré et est prévu pour des travaux futurs.

En conclusion, l'article documente la traduction réussie d'une théorie profonde de l'algèbre des opérateurs en un système formel utilisable, soulignant les compromis entre l'élégance mathématique et l'utilité pratique dans le contexte de la preuve de théorèmes interactive.