The continuous functional calculus in Lean

Sintesi Tecnica: Il Calcolo Funzionale Continuo in Lean

Enunciato del Problema
Il calcolo funzionale continuo è uno strumento fondamentale nella teoria delle $C^*$-algebre, che permette l'identificazione di sottocalcoli $C^*$ commutative con algebre di funzioni continue su spazi compatti Hausdorff. Sebbene sia matematicamente ben compreso, la sua formalizzazione in assistenti di prova come Lean presenta sfide significative. La difficoltà principale risiede nel bilanciare la fedeltà matematica con l'usabilità. Una definizione matematica "naturale" spesso si basa su tipi dipendenti (ad esempio, funzioni definite solo sullo spettro di un elemento) e strutture raggruppate (ad esempio, mappe continue come un tipo specifico). Sebbene questi siano rigorosi, creano attrito nelle prove formali: riscrivere le uguaglianze diventa difficile perché i tipi dipendono da elementi specifici, e la composizione di funzioni richiede la gestione di complessi coercizioni di sottotipi e prove di continuità. Gli autori hanno identificato che un design che privilegia la stretta semplicità matematica spesso fallisce i "test del lit never" (litmus tests) di usabilità pratica richiesti da una libreria come Mathlib.

Metodologia e Decisioni di Design
Gli autori hanno sviluppato una formalizzazione del calcolo funzionale continuo in Lean 4, integrata nella libreria Mathlib. La loro metodologia ha coinvolto un processo di design iterativo, passando da una definizione matematicamente "pura" a un'interfaccia "utilitaristica". Le decisioni chiave di design includono:

1. Unbundling e "Junk Values" (Valori Spazzatura):
   Invece di definire il calcolo funzionale come una mappa dal tipo delle funzioni continue sullo spettro $C(\sigma(a), \mathbb{C})$ all'algebra, gli autori hanno definito una funzione cfc che accetta qualsiasi funzione $f: \mathbb{C} \to \mathbb{C}$ e qualsiasi elemento $a$. Se $a$ non è normale o $f$ non è continua sullo spettro, la funzione restituisce un "valore spazzatura" (tipicamente 0).

   • Razionale: Questo permette agli utenti di scrivere espressioni come $f(a)$ senza dover prima dimostrare che $a$ è normale o che $f$ è continua. Questo imita l'approccio "scrivi prima, pensa dopo" della matematica informale, ritardando l'onere della prova fino a quando non è necessaria una proprietà non banale. Ciò consente anche una riscrittura (rw) fluida poiché i tipi degli argomenti non dipendono più dalle proprietà specifiche di $a$.

2. Astrazione Basata su Classi:
   Per gestire diversi anelli scalari ($\mathbb{C}$, $\mathbb{R}$, e $\mathbb{R}_{\ge 0}$) e diversi tipi di elementi (normali, autoaggiunti, non negativi), gli autori hanno implementato il calcolo come una classe di tipi ContinuousFunctionalCalculus.

   • Generalizzazione dei Predicati: La classe è parametrizzata da un predicato $p$ sugli elementi dell'algebra (ad esempio, IsStarNormal, IsSelfAdjoint, 0 ≤ a). Ciò consente a un'unica interfaccia di coprire vari casi senza duplicazione del codice.
   • Prop-Valued vs. Data: Le versioni precedenti includevano l' $*$-omomorfismo come dato. Tuttavia, per evitare problemi di uguaglianza definizionale (dove due diverse costruzioni della stessa mappa potrebbero non essere definizionamente uguali), il design finale rende la classe un Prop. Essa asserisce l'esistenza di un $*$-omomorfismo unico con specifiche proprietà, piuttosto che memorizzare la mappa stessa.

3. Gestione delle Algebre Non Unitarie:
   La formalizzazione si estende alle $C^*$-algebre non unitarie. Invece di fare affidamento su costruzioni estrinseche come la unitarizzazione minima per ogni definizione, gli autori hanno introdotto una definizione intrinseca di quasispettro. Il calcolo funzionale non unitario è definito su funzioni che annullano lo 0 (o mappano lo 0 in 0), evitando la necessità di passare costantemente tra contesti unitari e non unitari.

4. Automazione tramite autoParam:
   Per mitigare la verbosità del passaggio manuale di prove di continuità e normalità, gli autori hanno utilizzato la funzione autoParam di Lean. Le ipotesi come "f è continua sullo spettro" sono dotate di tattiche predefinite. Se l'utente non fornisce una prova, Lean tenta di sintetizzarla automaticamente utilizzando lemmi esistenti (ad esempio, aesop, fun_prop).

5. Unicità come Classe Separata:
   La proprietà di composizione ($g(f(a)) = (g \circ f)(a)$) è centrale nella teoria. Gli autori hanno dimostrato questo utilizzando un argomento di unicità piuttosto che il teorema di Stone–Weierstrass (che fallisce per $\mathbb{R}_{\ge 0}$). Hanno incapsulato l'unicità degli $*$-omomorfismi in una classe separata ContinuousMap.UniqueHom, permettendo alla proprietà di composizione di essere derivata genericamente attraverso diversi anelli scalari.

Contributi Chiave e Risultati

• Prima Formalizzazione: Questo lavoro costituisce la prima formalizzazione del calcolo funzionale continuo in qualsiasi assistente di prova.
• Integrazione in Mathlib: L'implementazione è unita a Mathlib, fornendo un'interfaccia unificata per i calcoli funzionali compli, reali e non negativi.
• Verifica dell'Usabilità: Il design è stato validato contro specifici "litmus tests", tra cui:
  • Definire gli inversi ($f(a^{-1})$) usando funzioni non continue ovunque (ad esempio, $x \mapsto x^{-1}$).
  • Costruire parti positive/negative e radici quadrate per elementi autoaggiunti e non negativi.
  • Applicare il calcolo a matrici su $\mathbb{R}$ (che mancano di una struttura metrica globale in Mathlib).
• Automazione: L'interfaccia supporta l'automazione di alto livello, consentendo agli utenti di dimostrare proprietà come $f(-a) = (x \mapsto f(-x))(a)$ con un intervento manuale minimo.
• Applicazioni: L'interfaccia è già stata utilizzata per formalizzare risultati avanzati, tra cui:
  • L'esistenza di unità approssimate nelle $C^*$-algebre non unitarie.
  • La continuità del calcolo funzionale in entrambe le variabili.
  • Proprietà di mappe $a \mapsto |a|$, $a \mapsto a^p$, e $a \mapsto \log(a)$.
  • Risultati riguardanti elementi unitari e proiezioni.

Significato e Limitazioni
Il documento rivendica importanza principalmente nella sua filosofia di design: dimostrare che, affinché uno strumento sia efficace in una libreria formale su larga scala, deve dare priorità all'ergonomia dell'utente finale (usabilità) rispetto alla stretta purezza matematica nella definizione. Accettando "valori spazzatura" e scompattando i tipi, gli autori hanno creato un'interfaccia che si comporta intuitivamente per i matematici, permettendo manipolazioni complesse (come composizione e riscrittura) che sarebbero proibitivamente difficili con un approccio basato strettamente sui tipi dipendenti.

Gli autori sono modesti riguardo allo stato attuale, riconoscendo alcune limitazioni:

• Lemmi Simp: A causa della necessità di argomenti espliciti per attivare autoParam, molti lemmi non possono essere usati come regole simp senza intervento manuale, rendendo alcune prove più verbiose del desiderato.
• Complicazioni di $\mathbb{R}_{\ge 0}$: L'uso dei numeri reali non negativi come anello scalare introduce ostacoli tecnici specifici (ad esempio, sottrazione troncata, mancanza di struttura di anello) che richiedono dichiarazioni di teoremi separate.
• $C^*$-algebre Reali: Sebbene il framework sia progettato per supportare le $C^*$-algebre reali, il caso specifico del calcolo funzionale su $\mathbb{C}$ per algebre reali (che richiede un dominio di funzioni diverso) non è ancora completamente integrato ed è pianificato per lavori futuri.

In conclusione, il documento documenta una riuscita traduzione di una profonda teoria dell'algebra degli operatori in un sistema formale utilizzabile, evidenziando i compromessi tra eleganza matematica e utilità pratica nel contesto della dimostrazione interattiva di teoremi.