Lean-21b : le lake mimo_lean par ses énoncés — compagnon formel natif
Compagnon natif du notebook Python Lean-21 : ici, plus de simulation — le lake mimo_lean est importé et exécuté dans un kernel Lean 4 réel, et chaque théorème est interrogé par #check / #print axioms avec sa signature rendue par le compilateur.
Ce compagnon comble le point noir mesuré par l’instrument de visibilité de l’EPIC #11703 : le module NormTails.lean n’était cité nulle part — le seul module du lake entièrement invisible, alors qu’il porte la Phase 3b, la concentration gaussienne du bruit, c’est-à-dire le travail de preuve le plus exigeant du lake (cf #11766).
Plan :
le lake et sa dépendance externe SLT — où passe la frontière entre ce qu’on a prouvé et ce qu’on a emprunté ;
NormTails : concentration de Lipschitz gaussienne — les déclarations, de la brique abstraite aux instanciations MIMO ;
Converse : Hanson–Wright, le cœur quantitatif du converse §11, et ses briques ;
Bridge : ce que le converse dit du décodeur ML — le pont vers l’apprentissage ;
exercices ;
briques utilitaires : Lmmse et Objective.
Pourquoi ce compagnon est précieux : dans un système de preuves, les énoncés sont la moitié du travail — l’autre moitié est la signature rendue par le compilateur, qui montre exactement ce que chaque théorème prouve et ce qu’il consomme (hypothèses, types, classes). #print axioms complète ce tableau en répertoriant les axiomes utilisés — un théorème qui repose sur sorry ou un axiome non-standard est immédiatement flaggé.
Le lac mimo_lean en bref : formalisation Lean 4 du papier Papailiopoulos 2026 sur la détection MIMO avec information au décodeur ML (Phase 1-4). Le lac contient les modules : Descent, Objective, Lmmse, Converse, Bridge, NormTails. La Phase 3b (NormTails) est la plus exigeante en termes de preuve — concentration de Lipschitz gaussienne, instantiation MIMO, queues de normes.
Coût global : ~10 secondes (import du lac + interrogations #check / #print axioms sur les déclarations).
1. Le lake et sa dépendance externe SLT
mimo_lean ne vit pas seul : il compose avec un lake externe vérifié, YuanheZ/lean-stat-learning-theory (SLT, Apache-2.0, sans sorry — au pin courant le lake requiert le fork jsboige/lean-stat-learning-theory @ 0b1020a, qui prouve la non-négativité de l’exposant à rayon nul d’Hanson–Wright au-dessus du pin amont d0f506f). C’est une propriété remarquable et pédagogiquement intéressante : la concentration de Lipschitz et l’inégalité de Hanson–Wright ne sont pas re-prouvées ici — elles sont empruntées à une bibliothèque externe dont chaque énoncé a été vérifié par le même noyau Lean. La cellule ci-dessous affiche le require du lakefile : c’est la frontière, écrite noir sur blanc.
Qu’est-ce que SLT ? : Statistical Learning Theory formalisée en Lean 4 par YuanheZ. Le dépôt GitHub héberge une bibliothèque de résultats standards en théorie statistique de l’apprentissage : concentration de Lipschitz pour gaussiennes (cf. GaussianLipConcen), inégalité de Hanson-Wright (cf. HansonWright), mesures gaussiennes standards (cf. GaussianMeasure), etc. Tous les énoncés sont vérifiés — pas de sorry, pas d’axiomes non-standard.
Pourquoi emprunter plutôt que re-prouver : la théorie de la concentration est un domaine mature avec des preuves bien établies. Les re-prouver dans mimo_lean serait du gaspillage — et introduirait un risque d’erreur. L’emprunt à une bibliothèque vérifiée est plus sûr que la duplication. C’est un principe de base de la vérification formelle : réutiliser ce qui est déjà prouvé.
La frontière emprunté/prouvé : dans le lakefile, le require slt from git est la ligne de partage. Tout ce qui est en amont de cette ligne (Mathlib, SLT) est emprunté (vérifié ailleurs). Tout ce qui est en aval (les modules de mimo_lean) est à prouver. Cette frontière est explicite dans le lakefile — c’est ce que la cellule code[0] affiche.
Sortie attendue (cellule code[0]) : un commentaire import listant les modules du lac, et un commentaire require listant les dépendances externes (Mathlib + SLT).
Coût : < 1 seconde (lecture de lakefile.lean, pas d’exécution de code).
-- Extrait de mimo_lean/lakefile.lean — la frontière entre prouvé et emprunté :
-- require slt from git
-- "https://github.com/jsboige/lean-stat-learning-theory.git" @ "0b1020a4771037b89d0b3809913608d177c09a14"
-- require mathlib from git
-- "https://github.com/leanprover-community/mathlib4.git" @ "db584cd6d46c92f209a44c0f1c829460d327499d"
-- (extrait verbatim du lakefile au HEAD ; toolchain v4.33.0 via lean-toolchain, migration #16341)
--
-- Les six modules du lake (Phase 1 -> 3b, puis pont ML) :
import Descent
import Objective
import Lmmse
import Converse
import Bridge
import NormTails
-- Extrait de mimo_lean/lakefile.lean — la frontière entre prouvé et emprunté :
-- (extrait verbatim du lakefile au HEAD ; toolchain v4.33.0 via lean-toolchain, migration #16341)
--
-- Les six modules du lake (Phase 1 -> 3b, puis pont ML) :
importDescent
importObjective
importLmmse
importConverse
importBridge
importNormTails
--% env 0
Raw input{"cmd": "-- Extrait de mimo_lean/lakefile.lean \u2014 la fronti\u00e8re entre prouv\u00e9 et emprunt\u00e9 :\n-- require slt from git\n-- \"https://github.com/jsboige/lean-stat-learning-theory.git\" @ \"0b1020a4771037b89d0b3809913608d177c09a14\"\n-- require mathlib from git\n-- \"https://github.com/leanprover-community/mathlib4.git\" @ \"db584cd6d46c92f209a44c0f1c829460d327499d\"\n-- (extrait verbatim du lakefile au HEAD ; toolchain v4.33.0 via lean-toolchain, migration #16341)\n--\n-- Les six modules du lake (Phase 1 -> 3b, puis pont ML) :\nimport Descent\nimport Objective\nimport Lmmse\nimport Converse\nimport Bridge\nimport NormTails"}Raw output{"env": 0}
1.1 Ce que SLT fournit — la partie empruntée
Deux théorèmes SLT sont consommés par le lake. Le premier (concentration de Lipschitz) alimente NormTails ; le second (Hanson–Wright) alimente le converse de Converse.lean. Décommenter mentalement les open : ils reflètent les open des fichiers sources.
Sortie de code[1] (verbatim tronque, cellule ci-dessous) : sous open GaussianLipConcen in, les deux #check rendent la version bilaterale et sa variante unilaterale.
Trois choses que la signature dit et qu’un resume perdrait. Le theoreme est generique en f et en L : il ne parle pas de la norme, il parle de n’importe quelle fonction L-lipschitzienne sur EuclideanSpace ℝ (Fin n) (le corps d’abord, le type d’indice ensuite). L’ecart est mesure a la moyenne∫ y, f y ∂μ, pas a zero. Et la variante gaussian_lipschitz_concentration_one_sided a la meme forme sans la valeur absolue, donc sans le facteur 2 devant l’exponentielle.
C’est la que se noue le lien avec la section 2 : mimo_lean specialise ce lemme en prenant pour f la norme euclidienne, qui est 1-Lipschitz. A L = 1, la conclusion devient exactement 2·exp(-t²/2) – la borne que code[6] evalue plus bas en quatre points.
Sortie de code[2] (verbatim tronque, cellule ci-dessous) : la cellule fait deux#check, et le second n’est pas decoratif.
HansonWright.hanson_wright_inequality {Ω : Type u_1} [MeasurableSpace Ω] {μ : Measure Ω}
[IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ}
{K C t : ℝ} (hK : 0 < K) (hC : 0 < C) (hC_domain : 4 * Real.exp 1 ≤ C) ...
(hF : 0 < frobeniusNorm A) (hOp : 0 < operatorNorm A)
(h_indep : iIndepFun X μ) (hX_subG : ∀ (i : Fin n), HasSubgaussianMGF (X i) ⟨K ^ 2, _⟩ μ)
(ht : 0 ≤ t) :
(μ {ω | t ≤ |centeredQuadraticForm μ A X ω|}).toReal
≤ 2 * Real.exp (-(1 / (4 * C)) * min (t ^ 2 / (K ^ 4 * frobeniusNorm A ^ 2))
(t / (K ^ 2 * operatorNorm A)))
GaussianMeasure.iIndepFun_eval_stdGaussianPi {n : ℕ} :
iIndepFun (fun i w => w i) (stdGaussianPi n)
Le double regime annonce est bien la – min d’un terme quadratique en t (petites deviations) et d’un terme lineaire (grandes) – mais avec les puissances de K qui comptent : t²/(K⁴‖A‖_F²) contre t/(K²‖A‖_op), le tout divise par 4C. En revanche l’hypothese n’est pas « covariance gaussienne standard » : c’est la sous-gaussianite coordonnee par coordonnee (HasSubgaussianMGF de parametre K²) plus l’independance. Le gaussien standard n’est qu’un cas particulier – et c’est precisement ce que decharge le second #check : iIndepFun_eval_stdGaussianPi certifie que les coordonnees de stdGaussianPi n sont independantes. Les contraintes numeriques sur C (4e ≤ C, 8e³ ≤ C, 16e ≤ C², 64e² ≤ C) fixent le domaine de validite de la constante.
Ce double regime est ce qui permet a la section 3 de fermer le converse sur toute la plage de t, la ou la borne de Lipschitz de la section 2 ne couvre que la norme.
Implication pour le lake : les theoremes SLT sont empruntés, pas prouvés ici. C’est une frontiere explicite, ecrite dans le lakefile.lean (cf. code[0] – le require slt from git montre la dependance externe). Le compilateur Lean verifie que la signature reste compatible au fil des commits, et la frontiere est auditable.
Premier emprunt — GaussianLipConcen : concentration sous-gaussienne pour fonctions Lipschitz. Si f est L-Lipschitz et X est un vecteur gaussien standard, alors f(X) est sous-gaussien de paramètre L. Cela donne la queue P(|f(X) - E[f(X)]| > t) ≤ 2·exp(-t²/(2L²)). Le théorème SLT est gaussian_lipschitz_concentration (two-sided) et gaussian_lipschitz_concentration_one_sided (one-sided). Le lac mimo_lean les consomme avec L = 1 (la norme euclidienne est 1-Lipschitz).
Second emprunt — HansonWright : inégalité de Hanson-Wright. Si X est un vecteur gaussien standard et A est une matrice, alors XᵀAX est sous-gaussien avec un paramètre qui dépend des normes de Frobenius et d’opérateur de A. C’est la brique technique qui permet de borner les formes quadratiques du bruit — alors que Lipschitz ne borne que les normes. Le théorème SLT est hanson_wright_inequality.
Le certificat d’indépendance : iIndepFun_eval_stdGaussianPi (dans GaussianMeasure) est un théorème technique qui certifie que les coordonnées d’un vecteur gaussien standard sont indépendantes. Le Converse.lean du lac l’utilise pour sommer les queues sur les N colonnes du canal.
Sortie attendue (cellules code[1]–[2]) : 4 #check produisant les signatures des théorèmes empruntés, sans erreur (les théorèmes sont définis dans SLT, donc #check rend leur type complet).
Coût : ~1 seconde (résolution open + #check).
-- Le theoreme de concentration derriere NormTails (SLT.GaussianLipConcen) :
open GaussianLipConcen in
#check gaussian_lipschitz_concentration
open GaussianLipConcen in
#check gaussian_lipschitz_concentration_one_sided
-- Le theoreme de concentration derriere NormTails (SLT.GaussianLipConcen) :
-- L'inegalite de Hanson-Wright derriere le converse (SLT.HansonWright) :
open HansonWright in
#check hanson_wright_inequality
-- et le certificat d'independance des coordonnees que Converse lui passe :
open GaussianMeasure in
#check iIndepFun_eval_stdGaussianPi
-- L'inegalite de Hanson-Wright derriere le converse (SLT.HansonWright) :
Raw input{"cmd": "-- L'inegalite de Hanson-Wright derriere le converse (SLT.HansonWright) :\nopen HansonWright in\n#check hanson_wright_inequality\n\n-- et le certificat d'independance des coordonnees que Converse lui passe :\nopen GaussianMeasure in\n#check iIndepFun_eval_stdGaussianPi", "env": 1}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"HansonWright.hanson_wright_inequality.{u_1} {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}\n [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {X : Fin n → Ω → ℝ} {K C t : ℝ}\n (hK : 0 < K) (hC : 0 < C) (hC_domain : 4 * Real.exp 1 ≤ C) (hC_diag_quad : 8 * Real.exp 1 ^ 3 ≤ C)\n (hC_offdiag_domain : 16 * Real.exp 1 ≤ C ^ 2) (hC_offdiag_quad : 64 * Real.exp 1 ^ 2 ≤ C) (hF : 0 < frobeniusNorm A)\n (hOp : 0 < operatorNorm A) (h_indep : ProbabilityTheory.iIndepFun X μ)\n (hX_subG : ∀ (i : Fin n), ProbabilityTheory.HasSubgaussianMGF (X i) ⟨K ^ 2, ⋯⟩ μ) (ht : 0 ≤ t) :\n (μ {ω | t ≤ |centeredQuadraticForm μ A X ω|}).toReal ≤\n 2 * Real.exp (-(1 / (4 * C)) * min (t ^ 2 / (K ^ 4 * frobeniusNorm A ^ 2)) (t / (K ^ 2 * operatorNorm A)))"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"GaussianMeasure.iIndepFun_eval_stdGaussianPi {n : ℕ} : ProbabilityTheory.iIndepFun (fun i w => w i) (stdGaussianPi n)"}],
"env": 2}
Tout le reste de ce notebook visite ce que mimo_leanajoute par-dessus ses imports : la spécialisation MIMO de la concentration (NormTails), le converse quantitatif (Converse) et son pont vers le décodeur ML (Bridge).
Modules porteurs + modules utilitaires :
Porteurs : NormTails, Converse, Bridge. Ce sont les modules qui portent le resultat mathematique du papier Papailiopoulos 2026 – la queue de la norme, le converse chi-carre, et le pont vers l’erreur ML.
Utilitaires : Descent (Phase 1), Objective (Phase 2), Lmmse (Phase 3a). Ce sont les briques de service : le point de depart de la minimisation, le cout de flip, la formule de trace gaussienne. Ils sont invoques par les modules porteurs mais ne portent pas un resultat novateur.
Pourquoi NormTails etait invisible : l’instrument de visibilite de l’EPIC #11703 a comptabilise aucune citation de NormTails dans le corpus Python/Lean, alors que Descent, Objective, Lmmse etaient cites plusieurs fois chacun. La raison est que NormTails est apparu tard dans le developpement du lake (Phase 3b), apres que la majorite du corpus Python ait ete ecrite. Ce compagnon comble ce trou documentaire : les declarations de NormTails sont maintenant interrogees par #check et leur role est explicite.
Difference avec le notebook Python : le notebook Lean-21 simule Monte-Carlo la queue de ‖w‖ et la compare a la borne. Ce compagnon-ci montre la borne elle-meme, signee par le compilateur Lean, sans simulation numerique. Les deux lectures sont complementaires : l’une pedagogique (intuition), l’autre formelle (certificat).
Trois ajouts spécifiques au lac :
Spécialisation MIMO : SLT donne la concentration en général, mais mimo_lean la spécialise au cas du bruit w gaussien standard de dimension M (M antennes de réception) et des colonnes h_i du canal (N antennes d’émission). Les déclarations noise_norm_tail, noise_norm_tail_one_sided, column_norm_tail sont les instanciations MIMO.
Converse quantitatif : SLT donne l’inégalité de Hanson-Wright en général, mais mimo_lean construit la chaîne chi-carré complète (cas A = 1, E‖w‖² = n, concentration de ‖w‖²). C’est un travail de glue entre plusieurs théorèmes SLT.
Pont vers le décodeur ML : SLT ne sait rien des décodeurs ML. mimo_leanconnecte la mécanique des flips (Phases 1-2) à la performance du décodeur ML (Phase 4) via Bridge.lean.
Pourquoi cette stratification est élégante : la pile de preuves suit une hiérarchie naturelle — théorie statistique (SLT) → spécialisation MIMO (mimo_lean) → application au décodeur ML (Bridge). Chaque couche ne connaît que la couche immédiatement inférieure. C’est une bonne pratique de vérification formelle : chaque module a une responsabilité unique.
Coût : pas de cellule code associée — c’est un paragraphe de transition.
2. NormTails — le module noir
La question physique du §11 du papier (Papailiopoulos 2026) : de combien la norme du bruit ‖w‖ peut-elle dévier de sa moyenne, et à quelle probabilité ? La norme euclidienne est une fonction 1-Lipschitz d’un vecteur gaussien standard ; la concentration sous-gaussienne de SLT donne alors, pour tout t > 0 :
C’est la queue de norme : elle borne uniformément les tailles ‖w‖ et ‖hᵢ‖ qui apparaissent dans le score de flip s·‖hᵢ‖² + √s·⟪hᵢ,w⟫. La route Lipschitz est la version « légère » du §11 — la queue chi-carré via Hanson–Wright (section 3) est le marteau-pilon pour la forme quadratique.
Architecture du module, en quatre briques :
Brique A : la norme euclidienne est 1-Lipschitz — le certificat Lipschitz que SLT consomme (norm_lipschitz_one).
Briques B : les théorèmes abstraits — concentration de ‖X‖ autour de sa moyenne pour X gaussien standard de dimension n (norm_concentration_one_sided et norm_concentration).
Brique C : instantiation MIMO — la queue de la norme du bruit ‖w‖ (M antennes) et la queue d’une colonne ‖h_i‖ du canal (noise_norm_tail_one_sided, noise_norm_tail, column_norm_tail).
Pourquoi cette architecture : la séparation entre abstrait (Briques A, B) et concret (Brique C) permet de réutiliser les théorèmes abstraits pour d’autres applications (pas seulement MIMO). C’est un principe de généricité en vérification formelle.
Le #print axioms : la cellule code[4] inclut #print axioms Mimo.norm_concentration qui liste les axiomes utilisés par ce théorème. Pour un théorème proprement prouvé, les axiomes sont uniquement propext, Classical.choice, Quot.sound — les axiomes standards de Lean. Aucun sorry, aucun axiome exotique.
Sortie attendue (cellules code[3]–[4]) : les #check + les #print axioms, montrant que les preuves reposent uniquement sur les axiomes standards.
-- Brique A : la norme euclidienne est 1-Lipschitz — le certificat que SLT consomme.
-- LipschitzWith 1 (fun x : EuclideanSpace R (Fin n) => ||x||)
open Mimo in
#check norm_lipschitz_one
-- Brique A : la norme euclidienne est 1-Lipschitz — le certificat que SLT consomme.
-- LipschitzWith 1 (fun x : EuclideanSpace R (Fin n) => ||x||)
Raw input{"cmd": "-- Brique A : la norme euclidienne est 1-Lipschitz \u2014 le certificat que SLT consomme.\n-- LipschitzWith 1 (fun x : EuclideanSpace R (Fin n) => ||x||)\nopen Mimo in\n#check norm_lipschitz_one", "env": 2}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 6},
"data": "Mimo.norm_lipschitz_one {n : ℕ} : LipschitzWith 1 fun x => ‖x‖"}],
"env": 3}
Lecture du lakefile et des modules (cellule code[0]) :
La cellule ci-dessus est un commentaire Lean qui simule le contenu du lakefile.lean. La structure typique d’un lakefile Lean 4 est :
require mathlib from git "...mathlib4.git" @ "db584cd6…"
require slt from git "...lean-stat-learning-theory.git" @ "..."
Les require déclarent les dépendances externes du lac. Pour mimo_lean, il y a 2 dépendances : Mathlib (la bibliothèque standard de Lean 4) et SLT (la théorie statistique de l’apprentissage).
Ensuite, les import listent les modules du lac lui-même. Pour mimo_lean :
Descent : Phase 1, l’algorithme de descente locale sur l’espace binaire {-1, +1}. Formalise la mécanique des flips bit-à-bit.
Objective : la fonction objectif MIMO s·‖h‖² + √s·⟪h,w⟫ — formelle mais sans contenu probabiliste.
Lmmse : la formule de la trace gaussienne, base du calcul LMMSE.
Converse : Phase 3, le converse quantitatif du §11 — Hanson-Wright
chi-carré + union bound.
Bridge : Phase 4, le pont entre mécanique des flips et performance du décodeur ML.
NormTails : Phase 3b, la concentration gaussienne du bruit (le « module noir » cité 0 fois dans le dépôt, comblé par ce compagnon).
Pourquoi cet ordre dans les imports : Lean n’impose pas d’ordre, mais l’ordre reflète les dépendances logiques : Lmmse et Objective sont utilitaires (pas de dépendance), Converse dépend de SLT et Lmmse, Bridge dépend de Converse, NormTails est le dernier module (Phase 3b la plus exigeante).
Coût : < 1 seconde (lecture de lakefile.lean).
-- Briques B : les theoremes abstraits — concentration de ||X|| autour de sa moyenne
-- pour X gaussien standard de dimension n (instances directes de SLT avec L = 1).
open Mimo in
#check norm_concentration_one_sided
open Mimo in
#check norm_concentration
-- Premiere lecture « preuve propre » : uniquement les axiomes standards de Lean.
#print axioms Mimo.norm_concentration
-- Briques B : les theoremes abstraits — concentration de ||X|| autour de sa moyenne
-- pour X gaussien standard de dimension n (instances directes de SLT avec L = 1).
Raw input{"cmd": "-- Briques B : les theoremes abstraits \u2014 concentration de ||X|| autour de sa moyenne\n-- pour X gaussien standard de dimension n (instances directes de SLT avec L = 1).\nopen Mimo in\n#check norm_concentration_one_sided\n\nopen Mimo in\n#check norm_concentration\n\n-- Premiere lecture \u00ab preuve propre \u00bb : uniquement les axiomes standards de Lean.\n#print axioms Mimo.norm_concentration", "env": 3}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 6},
"data":
"Mimo.norm_concentration_one_sided {n : ℕ} (hn : 0 < n) (t : ℝ) (ht : 0 < t) :\n ((GaussianMeasure.stdGaussianE n)\n {x | t ≤ ‖x‖ - ∫ (y : EuclideanSpace ℝ (Fin n)), ‖y‖ ∂GaussianMeasure.stdGaussianE n}).toReal ≤\n Real.exp (-t ^ 2 / 2)"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"Mimo.norm_concentration {n : ℕ} (hn : 0 < n) (t : ℝ) (ht : 0 < t) :\n ((GaussianMeasure.stdGaussianE n)\n {x | t ≤ |‖x‖ - ∫ (y : EuclideanSpace ℝ (Fin n)), ‖y‖ ∂GaussianMeasure.stdGaussianE n|}).toReal ≤\n 2 * Real.exp (-t ^ 2 / 2)"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 6},
"data":
"'Mimo.norm_concentration' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
"env": 4}
-- Brique C : instantiation MIMO — la queue de la norme du bruit ||w|| (M antennes).
-- Brique D : instantiation MIMO — la queue de la norme d'une colonne ||h_i|| du canal.
open Mimo in
#check noise_norm_tail_one_sided
open Mimo in
#check noise_norm_tail
open Mimo in
#check column_norm_tail
#print axioms Mimo.column_norm_tail
-- Brique C : instantiation MIMO — la queue de la norme du bruit ||w|| (M antennes).
-- Brique D : instantiation MIMO — la queue de la norme d'une colonne ||h_i|| du canal.
La queue 2·exp(−t²/2) décroît très vite. La cellule suivante l’évalue sur les premiers écarts-types, par quatre #eval consécutifs sur t = 1, 2, 3, 4 (la vérification Monte-Carlo empirique — la queue simulée sous la courbe — vit dans le notebook Python Lean-21).
Les quatre ordres de grandeur a attendre — la lecture verbatim de la sortie est faite plus bas, une fois la cellule executee :
t
2·exp(−t²/2)
ce que ca vaut
1
> 1
borne non-informative : elle depasse 1
2
≈ 0,27
exploitable : environ 27 %
3
≈ 0,022
sous 2,5 %
4
≈ 0,00067
sous 0,1 %
Implication pour le decodeur ML : si le decodeur est cense tolerer un bruit ‖w‖ qui s’ecarte de sa moyenne de t ecarts-types avec probabilite au plus p, alors la borne de concentration donne directement cette probabilite. Le notebook Python Lean-21 superpose la queue empirique a la borne theorique pour un n = M = 64 typique (64 antennes MIMO).
Pourquoi Float plutot que Real : #eval a besoin d’un type computable, et Float (IEEE 754 double precision) rend directement la valeur. L’affichage donne six decimales, ce qui laisse encore trois chiffres significatifs sur la plus petite des quatre valeurs (0.000671). Pour des evaluations plus precises, le lake utilise Real.exp (non affiche dans ce compagnon).
Pourquoi cette décroissance est rapide : la queue gaussienne est exponentielle en t², pas simplement exponentielle en t (comme la queue de Chernoff pour les variables bornées). Cela signifie qu’à 4 écarts-types, la probabilité est déjà ~10⁻³ — au-delà, elle devient astronomiquement petite. C’est ce qui rend les bornes de concentration gaussiennes si utiles en pratique.
Comparaison avec la borne de Chernoff : pour une variable bornée dans [0,1], la borne de Chernoff décroît en exp(-t²/2) aussi — mais pour une autre raison (Markov appliqué au moment d’ordre 2). Les deux bornes sont équivalentes en forme mais distinctes en hypothèse (gaussien continu vs bornée discrète). C’est l’unité profonde des bornes de concentration : la queue exponentielle en t² est la signature de la sous-gaussianité.
Sortie attendue (cellule code[6]) : 4 #eval Float calculant les valeurs exactes. Lean évalue l’expression 2 * Float.exp (-(t:Float) ^ 2 / 2) et imprime la valeur avec une précision arbitraire.
À trois écarts-types la borne tombe sous 2,5 %, à quatre sous 0,1 % : le bruit ne peut « s’échapper » que très rarement — c’est ce qui rend le score de flip stable.
Trois observations physiques :
Loi en exp(-t²/2) vs exp(-t) : la borne de concentration gaussienne est en exponentielle de t², pas de t. C’est la difference majeure avec la borne de Markov (P(X ≥ t) ≤ E[X]/t) ou la borne sous-exponentielle. Pour t = 4, exp(-16/2) = exp(-8) ≈ 3.35×10⁻⁴ (avant le facteur 2 de la borne symetrique), soit 0.000671 une fois double — exactement la valeur rendue par la cellule.
Facteur 2 dans 2·exp(-t²/2) : il vient du symetrique : on borne P(|‖X‖ - E‖X‖| ≥ t), qui est la reunion de P(‖X‖ - E‖X‖ ≥ t) et P(E‖X‖ - ‖X‖ ≥ t). La borne symetrique a donc un facteur 2 par rapport a la borne unilaterale.
Application au score de flip : dans le decodeur ML du papier Papailiopoulos, le score de flip est s·‖hᵢ‖² + √s·⟪hᵢ, w⟫. Le bruit ⟪hᵢ, w⟫ est un scalaire gaussien de variance ‖hᵢ‖², donc il s’ecarte de plus de 3 ecarts-types avec probabilite au plus ~0.0222 — c’est la borne de Chernoff ci-dessus, la queue gaussienne exacte valant 0.0027, huit fois moins (cf. section 3.1). Pour un decodeur avec N = 64 antennes, la probabilite qu’unhᵢ parmi les 64 ait un flip est bornee par 64 × 0.0222 ≈ 1.4, qui depasse encore 1 : l’union bound ne suffit pas – il faut la borne de Hanson-Wright (section 3) pour avoir une borne exponentiellement petite en n.
Transition vers la section 3 : la borne de Lipschitz borne la norme‖w‖, qui apparait lineairement dans le score de flip. Pour la forme quadratiquewᵀAw (qui apparait quand on ecrit l’erreur ML au carre), il faut une borne de Hanson-Wright, qui est le sujet de la section suivante.
L’intuition derrière la stabilité du score de flip : le score de flip est s·‖hᵢ‖² + √s·⟪hᵢ,w⟫. Le premier terme est déterministe (ne dépend pas du bruit). Le second terme est aléatoire et est ce qui peut faire « basculer » un flip. Or ⟪hᵢ,w⟫ ≤ ‖hᵢ‖·‖w‖ par Cauchy-Schwarz. Si ‖hᵢ‖ et ‖w‖ sont concentrés autour de leurs moyennes (c’est ce que NormTails prouve), alors ⟪hᵢ,w⟫ est lui-même concentré. Le score de flip ne peut s’échapper que lorsque les deux normes s’écartent simultanément — un événement doublement rare.
La loi des petits nombres appliquée au score de flip : la probabilité qu’un flip donné « batte » le point de départ est dominée par la queue de ‖w‖·‖hᵢ‖. Quand les deux queues sont indépendantes (cas gaussien), la probabilité combinée est le produit — d’où une probabilité extrêmement petite. C’est ce que Bridge.lean capture formellement.
Coût : pas de cellule code — c’est une interprétation.
Lecture des evaluations Float.exp (ancre sur code[6])
La sortie verbatim de code[6] montre quatre #eval consecutifs, avec un badge ─────▶ pour chaque resultat :
t = 1 : borne > 1 (non-informative pour la concentration, mais reflete quand meme la borne symetrique 2·exp(-1/2)).
t = 2 : borne ~ 0.27 (deja exploitable : la norme s’ecarte de plus de 2 ecarts-types avec probabilite environ 27%).
t = 3 : borne sous 2,5% (utile en pratique : 3 sigma est le seuil de la regle 68-95-99.7, et la borne theorique donne 0.022218).
t = 4 : borne sous 0,07% (excellent : la queue au-dela de 4 sigma est negligeable).
La decroissance est super-exponentielle : d’un ecart-type au suivant, le facteur n’est pas constant — 1.213 → 0.271 (÷4,5), puis 0.271 → 0.0222 (÷12), puis 0.0222 → 0.000671 (÷33). C’est la signature du t² a l’exposant : chaque ecart-type supplementaire coute de plus en plus cher.
Pourquoi Float plutot que Real : Real.exp est non-computable par defaut (la fonction exp reelle n’a pas d’algorithme exact en arithmetique flottante). Pour #eval, on a besoin d’un type computable, donc Float (IEEE 754 double precision). L’affichage a six decimales garde trois chiffres significatifs jusqu’a la plus petite des quatre valeurs (0.000671).
Implication pour la suite : la section 3 sur le converse Hanson-Wright prend la releve pour les formes quadratiques. La borne de Lipschitz est suffisante pour la norme, mais insuffisante pour wᵀAw. La frontiere entre les deux routes est tracee dans la documentation du module Converse.
3. Converse — Hanson–Wright, le cœur quantitatif du converse
La route lourde du §11 : au lieu de borner la norme (Lipschitz), on borne la forme quadratiquewᵀAw. L’inégalité de Hanson–Wright (empruntée à SLT) donne une queue en min(t²/‖A‖_F², t/‖A‖_op) — le cas A = 1 (identité) redonne la queue chi-carré de ‖w‖², avec E‖w‖² = n. C’est la brique « queues chi-squared » de la formalisation #11152 — χ² étant absent de Mathlib au pin courant (v4.33.0), elle est construite via Hanson–Wright plutôt que par une loi χ² dédiée.
Sortie de code[7] (verbatim tronque, cellule ci-dessous) : elle declare #check hanson_wright_noise apres open Mimo in, et la signature rendue est celle du theoreme central :
Mimo.hanson_wright_noise {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {C t : ℝ} (hC : 0 < C)
(hC₁ : 4 * Real.exp 1 ≤ C) (hC₂ : 8 * Real.exp 1 ^ 3 ≤ C) (hC₃ : 16 * Real.exp 1 ≤ C ^ 2)
(hC₄ : 64 * Real.exp 1 ^ 2 ≤ C) (hF : 0 < HansonWright.frobeniusNorm A)
(hOp : 0 < HansonWright.operatorNorm A) (ht : 0 ≤ t) :
((GaussianMeasure.stdGaussianPi n) {w | t ≤ |HansonWright.centeredQuadraticForm … w|}).toReal ≤
2 * Real.exp (-(1 / (4 * C)) *
min (t ^ 2 / HansonWright.frobeniusNorm A ^ 2) (t / HansonWright.operatorNorm A))
Les hypotheses ne sont pas des conditions de rang : ce sont quatre minorations portant sur la meme constante C (hC₁ a hC₄), plus la stricte positivite des deux normes de A (hF, hOp) et 0 ≤ t. La constante n’est donc pas fournie par le theoreme — c’est l’appelant qui choisit C assez grande, et 1/(4C) est le taux de decroissance qu’il obtient en echange. La meme cellule enchaine #print axioms Mimo.hanson_wright_noise.
Difference entre Hanson-Wright et Lipschitz :
Lipschitz borne ‖f(X) - Ef(X)‖ pour f 1-Lipschitz. Le cout est lineaire en t : P(|f(X) - Ef(X)| ≥ t) ≤ 2·exp(-t²/(2σ²)).
Hanson-Wright borne XᵀAX - E[XᵀAX] pour A symetrique. Le cout est en min(t²/‖A‖_F², t/‖A‖_op) : quadratique pour t petit, lineaire pour t grand.
Pourquoi les deux : pour borner la norme‖w‖, Lipschitz suffit (la norme est 1-Lipschitz). Pour borner la forme quadratiquewᵀAw qui apparait dans le calcul de l’erreur ML, il faut Hanson-Wright. Le lake expose les deux routes, et la section 3 specialise Hanson-Wright au cas MIMO.
Pourquoi Hanson-Wright et pas χ² directement : la loi du χ² est la distribution de ‖w‖² pour w gaussien standard (somme de n carrés indépendants). Mathlib au pin courant (v4.33.0) ne contient pas de théorie des χ² — il aurait fallu tout construire depuis zéro. Hanson-Wright est plus général (il s’applique à toute forme quadratique wᵀAw, pas seulement A = 1), et SLT le fournit déjà vérifié. La formalisation mimo_lean l’utilise donc comme raccourci pour le cas particulier A = 1.
Le min dans la borne : min(t²/‖A‖_F², t/‖A‖_op) capture deux régimes. Pour petitt, c’est t²/‖A‖_F² qui domine (régime sub-quadratique). Pour grandt, c’est t/‖A‖_op (régime linéaire, type Chernoff). Le minimum donne la meilleure borne dans les deux régimes. C’est un raffinement important par rapport à une borne « uniforme » en exp(-t) ou exp(-t²).
Sortie attendue (les trois cellules de code ci-dessous) : #check pour les théorèmes de glue (hanson_wright_noise, quadraticForm_one, frobeniusNormSq_one, frobeniusNorm_one_sq, operatorNorm_one) + #check pour la chaîne chi-carré (hasSubgaussianMGF_eval_stdGaussianPi, integral_sq_eval_stdGaussianPi, integral_sqnorm_stdGaussianPi, chisq_norm_concentration, gaussian_coordinate_escape_bound).
Coût : ~2 secondes (10 #check + 2 #print axioms).
-- Le coeur : Hanson-Wright pour le bruit gaussien standard. Quatre conditions de
-- taille sur la constante C, deux normes de A strictement positives, queue en
-- min(t^2/Frobenius^2, t/operatorNorm).
open Mimo in
#check hanson_wright_noise
#print axioms Mimo.hanson_wright_noise
-- Le coeur : Hanson-Wright pour le bruit gaussien standard. Quatre conditions de
-- taille sur la constante C, deux normes de A strictement positives, queue en
Raw input{"cmd": "-- Le coeur : Hanson-Wright pour le bruit gaussien standard. Quatre conditions de\n-- taille sur la constante C, deux normes de A strictement positives, queue en\n-- min(t^2/Frobenius^2, t/operatorNorm).\nopen Mimo in\n#check hanson_wright_noise\n\n#print axioms Mimo.hanson_wright_noise", "env": 6}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 5, "column": 0},
"endPos": {"line": 5, "column": 6},
"data":
"Mimo.hanson_wright_noise {n : ℕ} {A : Matrix (Fin n) (Fin n) ℝ} {C t : ℝ} (hC : 0 < C) (hC₁ : 4 * Real.exp 1 ≤ C)\n (hC₂ : 8 * Real.exp 1 ^ 3 ≤ C) (hC₃ : 16 * Real.exp 1 ≤ C ^ 2) (hC₄ : 64 * Real.exp 1 ^ 2 ≤ C)\n (hF : 0 < HansonWright.frobeniusNorm A) (hOp : 0 < HansonWright.operatorNorm A) (ht : 0 ≤ t) :\n ((GaussianMeasure.stdGaussianPi n)\n {w | t ≤ |HansonWright.centeredQuadraticForm (GaussianMeasure.stdGaussianPi n) A (fun i w => w i) w|}).toReal ≤\n 2 * Real.exp (-(1 / (4 * C)) * min (t ^ 2 / HansonWright.frobeniusNorm A ^ 2) (t / HansonWright.operatorNorm A))"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"'Mimo.hanson_wright_noise' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
"env": 7}
Lecture des théorèmes SLT empruntés (cellules code[1]–[2]) :
Les 4 #check rendent les signatures des théorèmes SLT consommés par le lac (les signatures complètes, verbatim, sont commentées en §1.1 ci-dessus).
gaussian_lipschitz_concentration (de GaussianLipConcen) : le théorème certifie qu’une fonction L-Lipschitz d’un vecteur gaussien standard a une queue sous-gaussienne — l’écart à la moyenne est borné par 2·exp(-t²/(2L²)). La sortie attendue par #check est juste le type — sans corps de preuve affiché.
gaussian_lipschitz_concentration_one_sided : variante one-sided — sans la valeur absolue autour de l’écart, donc sans le facteur 2 devant l’exponentielle.
hanson_wright_inequality (de HansonWright) : le théorème certifie qu’une forme quadratique centrée XᵀAX a une queue en min(t²/‖A‖_F², t/‖A‖_op) — c’est la brique technique des queues chi-carré.
iIndepFun_eval_stdGaussianPi (de GaussianMeasure) : un théorème technique qui certifie que les coordonnées d’un vecteur gaussien standard sont indépendantes (en tant que iIndepFun). Le Converse.lean l’utilise pour sommer les queues sur les N colonnes du canal MIMO.
Coût : ~1 seconde (résolution open + #check).
-- Les quatre lemmes de glue : le cas A = 1 (identite) qui redescend Hanson-Wright
-- vers la forme quadratique euclidienne somme des w_i^2.
open Mimo in
#check quadraticForm_one
open Mimo in
#check frobeniusNormSq_one
open Mimo in
#check frobeniusNorm_one_sq
open Mimo in
#check operatorNorm_one
-- Les quatre lemmes de glue : le cas A = 1 (identite) qui redescend Hanson-Wright
-- vers la forme quadratique euclidienne somme des w_i^2.
Raw input{"cmd": "-- Les quatre lemmes de glue : le cas A = 1 (identite) qui redescend Hanson-Wright\n-- vers la forme quadratique euclidienne somme des w_i^2.\nopen Mimo in\n#check quadraticForm_one\n\nopen Mimo in\n#check frobeniusNormSq_one\n\nopen Mimo in\n#check frobeniusNorm_one_sq\n\nopen Mimo in\n#check operatorNorm_one", "env": 7}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 6},
"data":
"Mimo.quadraticForm_one {n : ℕ} (w : Fin n → ℝ) : HansonWright.quadraticForm 1 w = ∑ i, w i * w i"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"Mimo.frobeniusNormSq_one {n : ℕ} : HansonWright.frobeniusNormSq 1 = ↑n"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 6},
"data":
"Mimo.frobeniusNorm_one_sq {n : ℕ} : HansonWright.frobeniusNorm 1 ^ 2 = ↑n"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data":
"Mimo.operatorNorm_one {n : ℕ} (hn : 0 < n) : HansonWright.operatorNorm 1 = 1"}],
"env": 8}
-- La chaine chi-carré : certificat sous-gaussien des coordonnees, second moment,
-- E||w||^2 = n, puis la concentration chi-carré de ||w||^2 (A = 1).
open Mimo in
#check hasSubgaussianMGF_eval_stdGaussianPi
open Mimo in
#check integral_sq_eval_stdGaussianPi
open Mimo in
#check integral_sqnorm_stdGaussianPi
open Mimo in
#check chisq_norm_concentration
open Mimo in
#check gaussian_coordinate_escape_bound
#print axioms Mimo.chisq_norm_concentration
-- La chaine chi-carré : certificat sous-gaussien des coordonnees, second moment,
-- E||w||^2 = n, puis la concentration chi-carré de ||w||^2 (A = 1).
Raw input{"cmd": "-- La chaine chi-carr\u00e9 : certificat sous-gaussien des coordonnees, second moment,\n-- E||w||^2 = n, puis la concentration chi-carr\u00e9 de ||w||^2 (A = 1).\nopen Mimo in\n#check hasSubgaussianMGF_eval_stdGaussianPi\n\nopen Mimo in\n#check integral_sq_eval_stdGaussianPi\n\nopen Mimo in\n#check integral_sqnorm_stdGaussianPi\n\nopen Mimo in\n#check chisq_norm_concentration\n\nopen Mimo in\n#check gaussian_coordinate_escape_bound\n\n#print axioms Mimo.chisq_norm_concentration", "env": 8}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 4, "column": 0},
"endPos": {"line": 4, "column": 6},
"data":
"Mimo.hasSubgaussianMGF_eval_stdGaussianPi {n : ℕ} (i : Fin n) :\n ProbabilityTheory.HasSubgaussianMGF (fun w => w i) 1 (GaussianMeasure.stdGaussianPi n)"},
{"severity": "info",
"pos": {"line": 7, "column": 0},
"endPos": {"line": 7, "column": 6},
"data":
"Mimo.integral_sq_eval_stdGaussianPi {n : ℕ} (i : Fin n) :\n ∫ (w : Fin n → ℝ), w i ^ 2 ∂GaussianMeasure.stdGaussianPi n = 1"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 6},
"data":
"Mimo.integral_sqnorm_stdGaussianPi {n : ℕ} : ∫ (w : Fin n → ℝ), ∑ i, w i * w i ∂GaussianMeasure.stdGaussianPi n = ↑n"},
{"severity": "info",
"pos": {"line": 13, "column": 0},
"endPos": {"line": 13, "column": 6},
"data":
"Mimo.chisq_norm_concentration {n : ℕ} (hn : 0 < n) {C t : ℝ} (hC : 0 < C) (hC₁ : 4 * Real.exp 1 ≤ C)\n (hC₂ : 8 * Real.exp 1 ^ 3 ≤ C) (hC₃ : 16 * Real.exp 1 ≤ C ^ 2) (hC₄ : 64 * Real.exp 1 ^ 2 ≤ C) (ht : 0 ≤ t) :\n ((GaussianMeasure.stdGaussianPi n) {w | t ≤ |∑ i, w i * w i - ↑n|}).toReal ≤\n 2 * Real.exp (-(1 / (4 * C)) * min (t ^ 2 / ↑n) t)"},
{"severity": "info",
"pos": {"line": 16, "column": 0},
"endPos": {"line": 16, "column": 6},
"data":
"Mimo.gaussian_coordinate_escape_bound {n : ℕ} {c ε : ℝ} (hn : 0 < n) (hε : 0 < ε) (hc : |c| + ε / 2 ≤ 2)\n (hp1 : ε * Real.exp (-2) / √(2 * Real.pi) ≤ 1) :\n ((GaussianMeasure.stdGaussianPi n) {w | ∀ (i : Fin n), w i ∉ Set.Ioc (c - ε / 2) (c + ε / 2)}).toReal ≤\n Real.exp (-(↑n * (ε * Real.exp (-2) / √(2 * Real.pi))))"},
{"severity": "info",
"pos": {"line": 18, "column": 0},
"endPos": {"line": 18, "column": 6},
"data":
"'Mimo.chisq_norm_concentration' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
"env": 9}
Lecture de norm_concentration et ses axiomes (cellule code[4]) :
La cellule ci-dessus inclut un #print axioms Mimo.norm_concentration — un audit formel des axiomes utilisés par ce théorème.
Résultat attendu :
'Mimo.norm_concentration' depends on axioms: [propext, Classical.choice, Quot.sound]
Les trois axiomes sont les axiomes standards de Lean : - propext : la propositional extensionality — deux propositions équivalentes sont égales. - Classical.choice : le choix classique — pour toute famille non-vide d’ensembles non-vides, il existe une fonction de choix. - Quot.sound : l’égalité des quotients — deux éléments équivalents ont la même image dans le quotient.
Aucun sorry, aucun axiome non-standard. C’est la garantie de correction formelle : le théorème est prouvé à partir des axiomes de base de Lean, pas à partir d’un axiome inventé ou d’un sorry.
Pourquoi cette vérification est cruciale : sans #print axioms, on ne peut pas distinguer un théorème prouvé d’un théorème qui repose sur un axiome non-défini. Un auteur malveillant (ou distrait) pourrait ajouter axiom my_special_axiom : True et ensuite « prouver » n’importe quoi. #print axioms ferme cette porte.
Le #print axioms Mimo.column_norm_tail de la cellule code[5] : même audit pour l’instanciation MIMO. Le résultat attendu est identique (propext, Classical.choice, Quot.sound) — ce qui confirme que la spécialisation MIMO n’introduit pas d’axiome exotique.
Coût : < 1 seconde (#print axioms ne fait que lister).
3.1 Masse gaussienne et union bound
Les briques techniques qui précèdent : minorer la masse d’un gaussien sur un intervalle (pour que l’échappement d’une coordonnée ait un coût mesurable), et l’union bound exponentielle (1−p)ⁿ ≤ e^{−np} qui combine les N colonnes.
Sortie de code[10] (verbatim, cellule ci-dessous) : #check gaussianPDFReal_lower_abs rend
Il n’y a pas de parametre ε : la minoration est uniforme sur une boule. Des que |x| ≤ R, la densite standard en x vaut au moins ce qu’elle vaut au bord, exp(-R²/2)/√(2π). C’est la forme la plus commode pour minorer une masse — integrer une constante sur un intervalle est immediat — et c’est exactement ce dont se servent les lemmes gaussian_interval_mass_lower* de la meme cellule.
Pourquoi minorer φ(x) sur une boule : la densite gaussienne est concentree autour de 0, donc l’integrale sur un voisinage de 0 represente la majorite de la masse. Pour les minorations de queues, on a besoin d’integrer φ sur des queues qui s’eloignent de 0 (par exemple, |x| > t), et ces queues sont exponentiellement petites. Pour les queues lointaines, c’est l’encadrement de Mills qui sert, et il porte sur l’integrale, pas sur la densite : P(X > x) ≥ (1/(x√(2π)))·(1 - 1/x²)·exp(-x²/2) pour x > 0. La densite elle-meme n’a pas besoin d’etre minoree finement : le lemme ci-dessus la borne par sa valeur au bord de la boule, ce qui suffit.
Application a l’union bound : la borne P(⋃ᵢ Eᵢ) ≤ Σᵢ P(Eᵢ) est l’union bound de Boole. Si les Eᵢ sont independants et ont chacun probabilite p, alors P(⋃ᵢ Eᵢ) = 1 - (1-p)ⁿ ≤ np. La version exponentielle va dans l’autre sens : P(⋃ᵢ Eᵢ) ≥ 1 - exp(-np), parce que 1 - p ≤ e^{-p} (convexite de l’exponentielle) donne (1-p)ⁿ ≤ e^{-np}. C’est ce sens-la qui sert un converse — on veut garantir qu’un echappement arrive, pas qu’il est rare.
Bridge vers le decodeur ML : pour N antennes et un seuil de tolerance t, la probabilite qu’au moins une antenne ait un bruit superieur a t ecarts-types est bornee par N · P(|X| > t). Pour t = 3 et N = 64, c’est 64 · 0.0027 ≈ 0.17 — ou 0.0027 est la queue gaussienne exacteP(|X| > 3), et non la borne 2·exp(-9/2) = 0.0222 de la section 2.1, qui donnerait 64 · 0.0222 ≈ 1.4 et ne fermerait pas. Pour t = 4, la queue exacte vaut 6.3×10⁻⁵, soit 64 · 6.3×10⁻⁵ ≈ 4×10⁻³. Pour les grandes antennes (MIMO massif), seule la borne de Hanson-Wright (avec sa dependance en min(t²/‖A‖_F², t/‖A‖_op)) permet de fermer.
Pourquoi minorer la masse gaussienne : la borne de Hanson-Wright dit que la queue est petite. Mais pour borner la performance du décodeur ML, on a besoin de minorer la masse sur l’intervalle central (près de 0) — sinon l’événement « le bruit est dans la boîte de déviation » peut être trop fréquent. Les théorèmes gaussianPDFReal_lower_abs, gaussianPDFReal_lower_two, gaussian_interval_mass_lower_param, gaussian_interval_mass_lower, gaussian_interval_mass_lower_inv_sqrt donnent ces minorations en closed form.
L’union bound exponentielle : si chaque colonne a une probabilité p d’« échapper » au décodeur ML, et si les colonnes sont indépendantes (garantie par iIndepFun_eval_stdGaussianPi de SLT), alors la probabilité qu’aucune n’échappe est (1-p)ⁿ. L’inégalité (1-p)ⁿ ≤ exp(-np) (cf. one_sub_pow_le_exp_mul) borne cette probabilité par une exponentielle simple. C’est la contrepartie quantitative du converse : elle garantit que des échappements se produisent, bornant par en dessous la performance atteignable du décodeur ML.
L’assemblage : la borne finale du décodeur ML est de forme 1 - exp(…) — la signature exacte de ml_error_prob_ge_threshold (section 4 ci-dessous) rend la forme explicite. Une minoration de la probabilité d’erreur est exactement ce qu’un converse doit produire : elle dit ce qu’aucun décodeur ne peut dépasser.
Sortie attendue (cellule code[10]) : #check pour les théorèmes de minoration + #check pour l’union bound exponentielle.
Coût : ~1 seconde (7 #check).
-- Minorations de la densite gaussienne (pres de 0, puis parametree) :
open Mimo in
#check gaussianPDFReal_lower_abs
open Mimo in
#check gaussianPDFReal_lower_two
open Mimo in
#check gaussian_interval_mass_lower_param
open Mimo in
#check gaussian_interval_mass_lower
open Mimo in
#check gaussian_interval_mass_lower_inv_sqrt
-- Union bound exponentielle : (1 - p)^n <= exp(-n*p) :
open Mimo in
#check one_sub_pow_le_exp_mul
-- Minorations de la densite gaussienne (pres de 0, puis parametree) :
La Phase 4 : relier la mécanique des flips (Phases 1–2, Descent/Objective) à la performance du décodeur ML. Le résultat final dit : si un flip « bat » le point de départ, alors l’erreur ML est dans la boîte de déviation {0, 2}^N — et la probabilité que l’erreur ML dépasse un seuil a une borne explicite, via les queues de NormTails et Converse.
Les declarations cles du module Bridge :
Sortie de code[11] (verbatim, cellule ci-dessous) : #check cost_diff rend le socle algebrique du pont — pas une inegalite, une identite :
Mimo.cost_diff {E} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (w z v : E) {s : ℝ} (hs : 0 ≤ s) :
‖w + √s • z + √s • v‖ ^ 2 - ‖w + √s • z‖ ^ 2
= s * ‖v‖ ^ 2 + 2 * √s * inner ℝ w v + 2 * s * inner ℝ z v
L’espace est un espace de Hilbert reel quelconque (InnerProductSpace ℝ E), pas un pre-hilbertien complexe : le developpement du carre de la norme n’a de terme croise simple que dans le cas reel. La lecture est directe — ajouter √s • v a un point coute un terme quadratique s‖v‖² et deux termes croises, dont un seul (2√s·⟪ w, v⟫) porte le bruit. C’est cette decomposition qui rend le cout d’un flip analysable coordonnee par coordonnee.
Sortie de code[12] (verbatim, cellule ci-dessous) : #check DeviationBox rend Mimo.DeviationBox (N : ℕ) : Set (Fin N → ℝ) — une partie de l’espace des vecteurs reels, pas un type de mots binaires : les erreurs vivent dans Fin N → ℝ. Son role se lit dans les lemmes que la meme cellule affiche autour d’elle : flipAt_mem_deviationBox (un flip appartient a la boite), flipAt_ne_zero, flip_bat_implies_mlError (un flip qui bat le point de depart force une erreur ML), et surtout la borne de queue
C’est ici, et non dans flip_bat_prob_lower, qu’apparait la forme 1 - exp(-…) — et c’est une minoration de la probabilite d’erreur, ce qu’un converse doit produire.
Sortie de code[13] (verbatim, cellule ci-dessous) : #check flip_bat_prob_lower est la borne par coordonnee, celle qu’on compose ensuite sur les N antennes :
Mimo.flip_bat_prob_lower {N M : ℕ} (A) {s : ℝ} (hs : 0 < s) (i : Fin N)
(hσ : 0 < ‖A (Pi.single i 1)‖) (hbound : √s * ‖A (Pi.single i 1)‖ ≤ 2) :
(2 - √s * ‖A (Pi.single i 1)‖) * Real.exp (-2) / √(2 * Real.pi)
≤ ((GaussianMeasure.stdGaussianPi …) {w | mimoObj A w s (flipAt i) < mimoObj A w s 0}).toReal
Il n’y a ni seuil δ ni probabilite p en argument : la minoration est explicite, elle ne depend que de √s · ‖A eᵢ‖ — la colonne i de A vue par Pi.single i 1 — et l’hypothese hbound borne cette quantite par 2, ce qui garde le facteur de gauche positif. La cellule affiche aussi no_flip_beats_prob_le, la version complementaire.
Implication pour la Section 5 : les exercices demandent a l’etudiant de lire ces signatures et de comprendre comment elles se composent. Le puzzle est : pourquoi la concatenation de cost_diff, DeviationBox, et flip_bat_prob_lower donne-t-elle la borne globale sur l’erreur ML ? La reponse tient en deux etapes : (1) si un flip bat le point de depart, alors l’erreur ML est dans la boite de deviation (Boite de deviation), et (2) la probabilite que l’erreur depasse un seuil est bornee par la queue composee.
L’architecture du Bridge :
Le socle : différence de coût d’un flip, soustraction mimoObj, résidu à zéro — formalise ce qu’est un flip qui bat le point de départ.
La face ML : boîte de déviation {0, 2}^N, erreur ML, et la chaîne flip → erreur ML. Formalise comment un flip cause une erreur ML.
Les bornes de probabilité : ferment le converse — relient les queues gaussiennes à la probabilité d’erreur.
Pourquoi cette architecture est élégante : elle sépare ce qui est vrai (le socle), ce qui se passe (la face ML), et à quelle fréquence (les bornes). C’est la triade classique définition → conséquence → quantification.
Le théorème final de Bridge : ml_error_prob_ge_thresholdminore la probabilité d’erreur ML par une quantité de forme 1 - exp(…) (signatures verbatim ci-dessus). C’est exactement ce qu’un converse doit produire — une limite inférieure, dérivée des queues de NormTails et Converse, qu’aucun décodeur ne peut dépasser.
Lecture des minorations de la densite gaussienne (ancre sur code[10])
La sortie verbatim de code[10] enumere les declarations. Certaines d’entre elles portent la substance :
open Mimo in
#check gaussianPDFReal_lower_abs
─────▶ Mimo.gaussianPDFReal_lower_abs {R x : ℝ} (hx : |x| ≤ R) :
Real.exp (-R ^ 2 / 2) / √(2 * Real.pi) ≤ ProbabilityTheory.gaussianPDFReal 0 1 x
#check one_sub_pow_le_exp_mul
─────▶ Mimo.one_sub_pow_le_exp_mul {n : ℕ} {p : ℝ} (hn : 0 < n) (hp0 : 0 ≤ p) (hp : p ≤ 1) :
(1 - p) ^ n ≤ Real.exp (-(↑n * p))
Les quatre autres sont gaussianPDFReal_lower_two, gaussian_interval_mass_lower_param, gaussian_interval_mass_lower et gaussian_interval_mass_lower_inv_sqrt — les variantes qui integrent la minoration ponctuelle sur un intervalle.
Trois roles :
Minorer la densite (gaussianPDFReal_lower_abs) : sur la boule |x| ≤ R, la densite standard vaut au moins sa valeur au bord. Minoration uniforme, sans parametre ε : c’est ce qui la rend integrable a la main.
Minorer une masse d’intervalle (gaussian_interval_mass_lower*) : integrer la constante precedente sur un intervalle donne une minoration de la masse gaussienne qu’il porte. C’est la brique dont se sert flip_bat_prob_lower pour produire son facteur exp(-2)/√(2π).
Composer sur les N colonnes (one_sub_pow_le_exp_mul) : (1-p)ⁿ ≤ exp(-np). Attention au sens de lecture — la probabilite qu’aucune des N colonnes ne s’ecarte est ainsi majoree par exp(-N·p), donc celle qu’au moins une s’ecarte est minoree par 1 - exp(-N·p). C’est bien une minoration : un converse doit garantir qu’un echappement se produit, pas qu’il est rare. L’hypothese hn : 0 < n est necessaire — l’enonce est faux pour n = 0, ou le membre de gauche vaut 1.
Composition dans le lake : ces briques se retrouvent dans la borne ml_error_prob_ge_threshold (cf. cell[27]), dont le membre de gauche 1 - exp(-(2·log N - log log N)) a exactement la forme produite par one_sub_pow_le_exp_mul une fois p instancie par la minoration de masse.
Pourquoi Real plutot que Float : les minorations de queues sont des inegalites continues, pas des evaluations ponctuelles. On les prouve une fois pour toutes et elles valent pour tout x reel. La precision flottante n’est pas requise pour la preuve – seulement pour l’evaluation (cf. Float.exp en cell[13]).
-- Le socle : difference de cout d'un flip, soustraction mimoObj, residu a zero :
open Mimo in
#check cost_diff
open Mimo in
#check mimoObj_sub_mimoObj
open Mimo in
#check mimoObj_residual_from_zero
open Mimo in
#check mimo_flip_cost_via_bridge
-- Les lemmes gaussiens techniques du pont :
open Mimo in
#check stdGaussianPi_map_toLp
open Mimo in
#check map_inner_stdGaussian
open Mimo in
#check gaussian_interval_mass_lower_open
-- Le socle : difference de cout d'un flip, soustraction mimoObj, residu a zero :
Raw input{"cmd": "-- Le socle : difference de cout d'un flip, soustraction mimoObj, residu a zero :\nopen Mimo in\n#check cost_diff\n\nopen Mimo in\n#check mimoObj_sub_mimoObj\n\nopen Mimo in\n#check mimoObj_residual_from_zero\n\nopen Mimo in\n#check mimo_flip_cost_via_bridge\n\n-- Les lemmes gaussiens techniques du pont :\nopen Mimo in\n#check stdGaussianPi_map_toLp\n\nopen Mimo in\n#check map_inner_stdGaussian\n\nopen Mimo in\n#check gaussian_interval_mass_lower_open", "env": 10}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"Mimo.cost_diff.{u_1} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (w z v : E) {s : ℝ} (hs : 0 ≤ s) :\n ‖w + √s • z + √s • v‖ ^ 2 - ‖w + √s • z‖ ^ 2 = s * ‖v‖ ^ 2 + 2 * √s * inner ℝ w v + 2 * s * inner ℝ z v"},
{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 6},
"data":
"Mimo.mimoObj_sub_mimoObj {N M : ℕ} (A : (Fin N → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin M)) (w : EuclideanSpace ℝ (Fin M))\n {s : ℝ} (hs : 0 ≤ s) (u u' : Fin N → ℝ) :\n mimoObj A w s u' - mimoObj A w s u =\n s * ‖A (u' - u)‖ ^ 2 + 2 * √s * inner ℝ (A (u' - u)) w + 2 * s * inner ℝ (A (u' - u)) (A u)"},
{"severity": "info",
"pos": {"line": 9, "column": 0},
"endPos": {"line": 9, "column": 6},
"data":
"Mimo.mimoObj_residual_from_zero {N M : ℕ} (A : (Fin N → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin M))\n (w : EuclideanSpace ℝ (Fin M)) {s : ℝ} (hs : 0 ≤ s) (v : Fin N → ℝ) :\n mimoObj A w s v - mimoObj A w s 0 = s * ‖A v‖ ^ 2 + 2 * √s * inner ℝ (A v) w"},
{"severity": "info",
"pos": {"line": 12, "column": 0},
"endPos": {"line": 12, "column": 6},
"data":
"Mimo.mimo_flip_cost_via_bridge {N M : ℕ} (A : (Fin N → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin M)) (w : EuclideanSpace ℝ (Fin M))\n {s : ℝ} (hs : 0 ≤ s) (i : Fin N) :\n mimoObj A w s (flipAt i) - mimoObj A w s 0 = 4 * (s * ‖A (Pi.single i 1)‖ ^ 2 + √s * inner ℝ (A (Pi.single i 1)) w)"},
{"severity": "info",
"pos": {"line": 16, "column": 0},
"endPos": {"line": 16, "column": 6},
"data":
"Mimo.stdGaussianPi_map_toLp {M : ℕ} :\n MeasureTheory.Measure.map (WithLp.toLp 2) (GaussianMeasure.stdGaussianPi M) =\n ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin M))"},
{"severity": "info",
"pos": {"line": 19, "column": 0},
"endPos": {"line": 19, "column": 6},
"data":
"Mimo.map_inner_stdGaussian {M : ℕ} (h : EuclideanSpace ℝ (Fin M)) :\n MeasureTheory.Measure.map (fun w => inner ℝ h w) (ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin M))) =\n ProbabilityTheory.gaussianReal 0 (‖h‖ ^ 2).toNNReal"},
{"severity": "info",
"pos": {"line": 22, "column": 0},
"endPos": {"line": 22, "column": 6},
"data":
"Mimo.gaussian_interval_mass_lower_open {a b : ℝ} (hab : a ≤ b) (ha : |a| ≤ 2) (hb : |b| ≤ 2) :\n (b - a) * Real.exp (-2) / √(2 * Real.pi) ≤ ((ProbabilityTheory.gaussianReal 0 1) (Set.Ioo a b)).toReal"}],
"env": 11}
-- La face ML : boite de deviation {0,2}^N, erreur ML, et la chaine flip -> erreur :
open Mimo in
#check DeviationBox
open Mimo in
#check mlError
open Mimo in
#check flipAt_mem_deviationBox
open Mimo in
#check flipAt_ne_zero
open Mimo in
#check flip_bat_implies_mlError
open Mimo in
#check ml_error_prob_ge_threshold
-- La face ML : boite de deviation {0,2}^N, erreur ML, et la chaine flip -> erreur :
Raw input{"cmd": "-- Les bornes de probabilite qui ferment le converse :\nopen Mimo in\n#check flip_bat_prob_lower\n\nopen Mimo in\n#check no_flip_beats_prob_le", "env": 12}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 3, "column": 0},
"endPos": {"line": 3, "column": 6},
"data":
"Mimo.flip_bat_prob_lower {N M : ℕ} (A : (Fin N → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin M)) {s : ℝ} (hs : 0 < s) (i : Fin N)\n (hσ : 0 < ‖A (Pi.single i 1)‖) (hbound : √s * ‖A (Pi.single i 1)‖ ≤ 2) :\n (2 - √s * ‖A (Pi.single i 1)‖) * Real.exp (-2) / √(2 * Real.pi) ≤\n ((ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin M))) {w | mimoObj A w s (flipAt i) < mimoObj A w s 0}).toReal"},
{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 6},
"data":
"Mimo.no_flip_beats_prob_le {N M : ℕ} (hM : 0 < M) (A : (Fin N → ℝ) →ₗ[ℝ] EuclideanSpace ℝ (Fin M)) {s c ε : ℝ}\n (hε : 0 < ε) (hc : |c| + ε / 2 ≤ 2) (hp1 : ε * Real.exp (-2) / √(2 * Real.pi) ≤ 1)\n (hcover :\n ∀ (w : EuclideanSpace ℝ (Fin M)),\n (∃ j, w.ofLp j ∈ Set.Ioc (c - ε / 2) (c + ε / 2)) → ∃ i, mimoObj A w s (flipAt i) < mimoObj A w s 0) :\n ((ProbabilityTheory.stdGaussian (EuclideanSpace ℝ (Fin M)))\n {w | ∀ (i : Fin N), ¬mimoObj A w s (flipAt i) < mimoObj A w s 0}).toReal ≤\n Real.exp (-(↑M * (ε * Real.exp (-2) / √(2 * Real.pi))))"}],
"env": 13}
5. Exercices
Chaque exercice se traite en décommentant le #check (ou le #print axioms) et en lisant la signature rendue par le compilateur. Les indices sont dans les commentaires.
Sortie de code[14] (cellule ci-dessous) : elle porte quatre exercices, tous en commentaire, et un seul #check actif.
Les quatre enonces commentes pointent respectivement gaussian_lipschitz_concentration (indice : « avec une constante L »), la paire noise_norm_tail / noise_norm_tail_one_sided, chisq_norm_concentration (le cas A = 1 de Hanson-Wright), et ml_error_prob_ge_threshold avec DeviationBox. Un #print axioms Mimo.hanson_wright_noise est commente au meme titre.
La seule ligne executee est #check 1 + 1, qui rend 1 + 1 : ℕ — et un commentaire de la cellule explique pourquoi : une cellule entierement commentee ferait echouer le kernel Lean sur unexpected end of input. Le #check trivial est donc un garde-fou de cellule, pas un exercice.
Pour traiter le premier exercice, l’etudiant decommente son #check et compare la signature de gaussian_lipschitz_concentration (lake externe SLT) avec l’usage qu’en fait mimo_lean : la specialisation consiste a fixer le type d’espace euclidien (par exemple EuclideanSpace ℝ (Fin n)) et a prendre la norme euclidienne comme fonction 1-Lipschitz — d’ou l’indice sur la constante L.
Pourquoi cet exercice : la competence visee est la lecture croisee de signatures. Un mathematicien applique doit pouvoir naviguer entre les modules d’un lake et reconnaitre les patterns : chisq_norm_concentration (exercice 3, route quadratique) se deduit-il de gaussian_lipschitz_concentration (exercice 1, route Lipschitz), ou les deux routes sont-elles distinctes ? La section 3 donne l’element de reponse — la borne de Lipschitz suffit pour la norme, pas pour la forme quadratique wᵀAw.
Conseil methodologique : ouvrir les deux fichiers source (mimo_lean/NormTails.lean et le module SLT correspondant) en parallele, et reperer les def, lemma, theorem qui ont la meme tete. La specialisation apparait generalement comme une instance ou un abbrev qui fixe certains parametres generiques.
Transition vers la section 6 : apres les exercices, le compagnon visite les briques utilitaires Lmmse (trace gaussienne) et Objective (Pythagore reel), qui sont les complements logistiques des modules porteurs.
Barème indicatif (Exercice 1) : 5-10 minutes (lecture du source SLT + identification de l’instance).
-- Exercice 1 : quel theoreme SLT se cache derriere norm_concentration ?
-- (indice : il est importe par SLT.GaussianLipConcen, avec une constante L)
-- open GaussianLipConcen in
-- #check gaussian_lipschitz_concentration
-- Exercice 2 : quelle est la difference entre noise_norm_tail et
-- noise_norm_tail_one_sided ? (indice : comparez le membre de gauche des
-- deux enonces — valeur absolue contre deviation simple)
-- open Mimo in
-- #check noise_norm_tail
-- open Mimo in
-- #check noise_norm_tail_one_sided
-- Exercice 3 : le marteau-pilon chi-carré. Que devient Hanson-Wright quand
-- A = 1 ? (indice : lisez l'enonce de chisq_norm_concentration et cherchez
-- ou Frobenius et operatorNorm de l'identite ont disparu)
-- open Mimo in
-- #check chisq_norm_concentration
-- Exercice 4 : la borne de l'erreur ML. Quelles hypotheses porte
-- ml_error_prob_ge_threshold, et que dit-elle sur DeviationBox ?
-- open Mimo in
-- #check ml_error_prob_ge_threshold
-- Pour aller plus loin : verifiez que hanson_wright_noise ne depend
-- d'aucun axiome exotique.
-- #print axioms Mimo.hanson_wright_noise
-- Commande neutre : une cellule 100 % commentaires fait lever
-- "unexpected end of input" au kernel lean4 (le parseur attend une commande
-- et rencontre l'EOF). Decommentez les exercices ci-dessus pour les activer.
#check 1 + 1
-- Exercice 1 : quel theoreme SLT se cache derriere norm_concentration ?
-- (indice : il est importe par SLT.GaussianLipConcen, avec une constante L)
-- open GaussianLipConcen in
-- #check gaussian_lipschitz_concentration
-- Exercice 2 : quelle est la difference entre noise_norm_tail et
-- noise_norm_tail_one_sided ? (indice : comparez le membre de gauche des
-- deux enonces — valeur absolue contre deviation simple)
-- open Mimo in
-- #check noise_norm_tail
-- open Mimo in
-- #check noise_norm_tail_one_sided
-- Exercice 3 : le marteau-pilon chi-carré. Que devient Hanson-Wright quand
-- A = 1 ? (indice : lisez l'enonce de chisq_norm_concentration et cherchez
-- ou Frobenius et operatorNorm de l'identite ont disparu)
-- open Mimo in
-- #check chisq_norm_concentration
-- Exercice 4 : la borne de l'erreur ML. Quelles hypotheses porte
-- ml_error_prob_ge_threshold, et que dit-elle sur DeviationBox ?
-- open Mimo in
-- #check ml_error_prob_ge_threshold
-- Pour aller plus loin : verifiez que hanson_wright_noise ne depend
-- d'aucun axiome exotique.
-- #print axioms Mimo.hanson_wright_noise
-- Commande neutre : une cellule 100 % commentaires fait lever
-- "unexpected end of input" au kernel lean4 (le parseur attend une commande
-- et rencontre l'EOF). Decommentez les exercices ci-dessus pour les activer.
1+1:ℕ
--% env 14
Raw input{"cmd": "-- Exercice 1 : quel theoreme SLT se cache derriere norm_concentration ?\n-- (indice : il est importe par SLT.GaussianLipConcen, avec une constante L)\n-- open GaussianLipConcen in\n-- #check gaussian_lipschitz_concentration\n\n-- Exercice 2 : quelle est la difference entre noise_norm_tail et\n-- noise_norm_tail_one_sided ? (indice : comparez le membre de gauche des\n-- deux enonces \u2014 valeur absolue contre deviation simple)\n-- open Mimo in\n-- #check noise_norm_tail\n-- open Mimo in\n-- #check noise_norm_tail_one_sided\n\n-- Exercice 3 : le marteau-pilon chi-carr\u00e9. Que devient Hanson-Wright quand\n-- A = 1 ? (indice : lisez l'enonce de chisq_norm_concentration et cherchez\n-- ou Frobenius et operatorNorm de l'identite ont disparu)\n-- open Mimo in\n-- #check chisq_norm_concentration\n\n-- Exercice 4 : la borne de l'erreur ML. Quelles hypotheses porte\n-- ml_error_prob_ge_threshold, et que dit-elle sur DeviationBox ?\n-- open Mimo in\n-- #check ml_error_prob_ge_threshold\n\n-- Pour aller plus loin : verifiez que hanson_wright_noise ne depend\n-- d'aucun axiome exotique.\n-- #print axioms Mimo.hanson_wright_noise\n\n-- Commande neutre : une cellule 100 % commentaires fait lever\n-- \"unexpected end of input\" au kernel lean4 (le parseur attend une commande\n-- et rencontre l'EOF). Decommentez les exercices ci-dessus pour les activer.\n#check 1 + 1\n", "env": 13}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 32, "column": 0},
"endPos": {"line": 32, "column": 6},
"data": "1 + 1 : ℕ"}],
"env": 14}
6. Les briques utilitaires : Lmmse et Objective
Les sections précédentes visitaient NormTails, Converse et Bridge. Il reste des modules utilitaires que l’instrument de visibilité de l’EPIC #11703 signalait comme partiellement invisibles : chacun porte une brique prouvée que le corpus ne citait nulle part. Ce sont des lemmes de service — mais ils ont un contenu propre : le premier dit pourquoi le second moment d’un vecteur gaussien se lit sur la diagonale de sa covariance ; le second est le Pythagore réel du coût de flip, redérivé pas à pas plutôt qu’invoqué.
Ce que la cellule suivante affiche : des #check et leurs #print axioms. Le premier lemme, integral_norm_sq_eq_trace, porte la formule de la trace gaussienne — pour une gaussienne centree de covariance B, E[‖x‖²] = tr B — sous l’hypothese B.PosSemidef. Le second, norm_add_sq_two, est le Pythagore reel‖x + y‖² = ‖x‖² + 2⟪x, y⟫ + ‖y‖², generique sur tout espace prehilbertien reel. La lecture detaillee des deux signatures vient apres la cellule (section 6.1).
Pourquoi ces briques comptent : sans la formule de la trace, on ne saurait pas calculer l’erreur de reconstruction d’un estimateur MMSE — c’est elle qui relie la geometrie euclidienne (‖·‖²) a la theorie des probabilites (E), et qui fait que la quantite qu’on cherche a borner en evaluant un decodeur se lit sur une diagonale.
Lien avec la section 4 : norm_add_sq_two est redérive des lemmes fondamentaux de Mathlib (inner_add_left, real_inner_comm) plutot qu’invoque en boite noire. Le cost_diff de la section 4 n’est pas ce lemme : c’en est la specialisation au cout d’un flip, avec le facteur d’echelle √s et les deux termes croises que le Pythagore generique ne porte pas. C’est le meme calcul, applique deux fois a des arguments differents.
Avant NormTails et Converse, des modules utilitaires plus simples. Lmmse contient la formule de la trace gaussienne : pour une gaussienne centrée de covariance B, E[‖x‖²] = tr B (version formalisée dans le lac, cf. integral_norm_sq_eq_trace ci-dessous). C’est la base du calcul de l’erreur quadratique moyenne du LMMSE (Linear Minimum Mean Square Error). Objective contient la fonction objectif MIMO : mimoObj(s; h, w) = s·‖h‖² + √s·⟪h,w⟫ — c’est le score de flip formel.
Pourquoi ces modules sont utilitaires : ils ne portent pas de résultats difficiles en théorie statistique. Ils sont nécessaires au pipeline mais pas suffisants pour la garantie de correction. C’est NormTails + Converse qui portent la difficulté.
Lmmse.lean : la trace gaussienne est un résultat classique en probabilité. Sa formalisation Lean est directe — pas de lemme technique, juste le calcul des intégrales gaussianes standards (que Mathlib fournit déjà). C’est un exemple de théorème facile à formaliser — la difficulté est dans NormTails et Converse.
Objective.lean : la fonction objectif est définie comme une simple expression arithmétique. Sa formalisation est triviale — c’est juste une définition (avec le mot-clé def). Ce qui est difficile c’est d’analyser cette fonction (monotonicité, convexité, comportement asymptotique) — mais c’est le travail de Converse.lean et Bridge.lean, pas d’Objective.lean.
-- Brique Lmmse : la formule de la trace gaussienne -- pour une gaussienne
-- centree de covariance B, E[||x||^2] = tr B : chaque coordonnee contribue
-- sa variance B i i (la moyenne etant nulle). PosSemidef n'est pas decoratif :
-- il porte l'existence meme de la mesure gaussienne.
open Mimo in
#check @integral_norm_sq_eq_trace
-- Ses axiomes -- que Mathlib suffit, aucun axiome maison :
open Mimo in
#print axioms integral_norm_sq_eq_trace
-- Brique Objective : Pythagore reel -- ||x+y||^2 = ||x||^2 + 2<x,y> + ||y||^2,
-- rederive des lemmes fondamentaux (inner_add_left/right, real_inner_comm) :
open Mimo in
#check @norm_add_sq_two
open Mimo in
#print axioms norm_add_sq_two
-- Brique Lmmse : la formule de la trace gaussienne -- pour une gaussienne
-- centree de covariance B, E[||x||^2] = tr B : chaque coordonnee contribue
-- sa variance B i i (la moyenne etant nulle). PosSemidef n'est pas decoratif :
-- il porte l'existence meme de la mesure gaussienne.
Raw input{"cmd": "-- Brique Lmmse : la formule de la trace gaussienne -- pour une gaussienne\n-- centree de covariance B, E[||x||^2] = tr B : chaque coordonnee contribue\n-- sa variance B i i (la moyenne etant nulle). PosSemidef n'est pas decoratif :\n-- il porte l'existence meme de la mesure gaussienne.\nopen Mimo in\n#check @integral_norm_sq_eq_trace\n\n-- Ses axiomes -- que Mathlib suffit, aucun axiome maison :\nopen Mimo in\n#print axioms integral_norm_sq_eq_trace\n\n-- Brique Objective : Pythagore reel -- ||x+y||^2 = ||x||^2 + 2 + ||y||^2,\n-- rederive des lemmes fondamentaux (inner_add_left/right, real_inner_comm) :\nopen Mimo in\n#check @norm_add_sq_two\n\nopen Mimo in\n#print axioms norm_add_sq_two\n", "env": 14}Raw output{"messages":
[{"severity": "info",
"pos": {"line": 6, "column": 0},
"endPos": {"line": 6, "column": 6},
"data":
"@integral_norm_sq_eq_trace : ∀ {n : ℕ} {B : Matrix (Fin n) (Fin n) ℝ},\n B.PosSemidef → ∫ (x : EuclideanSpace ℝ (Fin n)), ‖x‖ ^ 2 ∂ProbabilityTheory.multivariateGaussian 0 B = B.trace"},
{"severity": "info",
"pos": {"line": 10, "column": 0},
"endPos": {"line": 10, "column": 6},
"data":
"'Mimo.integral_norm_sq_eq_trace' depends on axioms: [propext, Classical.choice, Quot.sound]"},
{"severity": "info",
"pos": {"line": 15, "column": 0},
"endPos": {"line": 15, "column": 6},
"data":
"@norm_add_sq_two : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (x y : E),\n ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * inner ℝ x y + ‖y‖ ^ 2"},
{"severity": "info",
"pos": {"line": 18, "column": 0},
"endPos": {"line": 18, "column": 6},
"data":
"'Mimo.norm_add_sq_two' depends on axioms: [propext, Classical.choice, Quot.sound]"}],
"env": 15}
Le compilateur a rendu les deux signatures, et elles méritent une lecture attentive.
La trace gaussienne (Lmmse). L’énoncé dit exactement : pour une matrice B semi-définie positive, l’intégrale de ‖x‖² contre la gaussienne multivariée de moyenne 0 et de covariance B égale B.trace. Chaque coordonnée contribue sa variance B i i — la moyenne étant nulle, il ne reste que le second moment, et la géométrie euclidienne le lit sur la diagonale. L’hypothèse B.PosSemidef n’est pas décorative : c’est elle qui garantit l’existence même de la mesure gaussienne (une covariance doit être semi-définie positive pour définir une loi). C’est la brique que l’estimateur MMSE du compagnon Python mobilise quand il évalue la qualité d’une reconstruction : l’erreur résiduelle se lit elle aussi comme une trace.
Le Pythagore réel (Objective). L’énoncé est générique sur tout espace préhilbertien réel E : ‖x + y‖² = ‖x‖² + 2⟪x, y⟫ + ‖y‖². En substituant y → -y, on obtient la décomposition du coût de flip du converse : ‖x - y‖² = ‖x‖² - 2⟪x, y⟫ + ‖y‖² — le terme central, le produit scalaire, mesure l’alignement entre le signal et la perturbation, et c’est lui que la borne de Hanson–Wright contrôle. Le lemme est redérivé des briques fondamentales (inner_add_left, real_inner_comm), pas invoqué comme une boîte noire.
Les axiomes — le certificat d’honnêteté. Les #print axioms rendent la même liste : [propext, Classical.choice, Quot.sound]. Ce sont les trois axiomes logiques standard que Mathlib assume partout — autrement dit, aucun axiome maison : ces deux lemmes sont prouvés de bout en bout, au même titre que le reste du lake.
L’élégance de Lean : le compilateur Lean rend toutes les contraintes implicites (positive_semidef, s ≥ 0, …) explicitement. C’est ce qui rend la formalisation vérifiable — chaque contrainte est soit prouvée, soit évidente par construction.
Conclusion
Le compagnon a visité les déclarations des modules porteurs du converse — NormTails (l’ancien point noir), Converse et Bridge — chacune interrogée par #check avec sa signature réelle, et sondée par #print axioms sur les théorèmes clés : uniquement les trois axiomes standards de Lean (propext, Classical.choice, Quot.sound), aucun sorry.
Deux lectures à retenir :
la frontière SLT — le lake compose avec une bibliothèque externe vérifiée ; la concentration de Lipschitz et Hanson–Wright sont empruntées, tout le reste (l’instanciation MIMO, le converse chi-carré, le pont ML) est prouvé ici ;
deux routes pour une même queue — la route légère (Lipschitz, NormTails) borne la norme, la route lourde (Hanson–Wright, Converse) borne la forme quadratique ; le pont Bridge convertit ces queues en borne sur l’erreur du décodeur ML.
La contrepartie expérimentale — Monte-Carlo de la queue de ‖w‖ superposée à la borne prouvée — vit dans le notebook Python Lean-21. Les modules Descent, Objective et Lmmse (Phases 1–3a) y sont également visités par leurs énoncés.
Le lac mimo_lean est un exemple de stratification propre : Mathlib (base arithmétique) → SLT (concentration statistique) → mimo_lean/NormTails (spécialisation Lipschitz MIMO) → mimo_lean/Converse (Hanson-Wright et chi-carré) → mimo_lean/Bridge (performance du décodeur ML). Chaque couche dépend de la précédente, mais ne la connaît pas en détail — l’emprunt à SLT est opaque pour mimo_lean/Converse, qui ne manipule que les énoncés de concentration, pas leurs preuves.
Trois leçons à retenir :
L’emprunt vérifié est plus sûr que la duplication. mimo_lean ne re-prouve pas la concentration de Lipschitz — il emprunte SLT. C’est plus sûr (la preuve est vérifiée par les mainteneurs SLT) et plus efficace (gain de temps de formalisation). Le coût est la dépendance externe — si SLT évolue, mimo_lean doit suivre.
La stratification permet la réutilisation. Les briques abstraites (norm_lipschitz_one, norm_concentration) sont séparées des briques concrètes (noise_norm_tail, column_norm_tail). On peut réutiliser les briques abstraites pour d’autres applications que MIMO.
Le #print axioms est un garde-fou essentiel. Pour chaque théorème important, on vérifie qu’il repose uniquement sur les axiomes standards de Lean (propext, Classical.choice, Quot.sound). Aucun sorry, aucun axiome exotique. C’est la garantie de correction.
Vers la suite : le notebook Python Lean-21 (déjà publié) montre la vérification empirique des bornes de NormTails via simulation Monte-Carlo. Les bornes théoriques y sont comparées aux fréquences empiriques — un bon test de cohérence entre théorie et simulation.
Coût global du notebook : ~10 secondes (lecture du lakefile + #check + #print axioms + #eval Float).