fix(lean,#17357): Lean-21 F1/F3/F4 -- prose alignee sur la borne reelle noise_norm_tail

MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21-MIMO-Detection-Flips.ipynb

@@ -512,8 +512,7 @@
     "\n",
     "print(\"--- lake env lean : les quatre theoremes phases (chargement de l'environnement) ---\")\n",
     "run_lean_snippet(SNIPPET_PHASES, \"phases\")\n",
-    "print(\"Sortie ci-dessus : declarations RELLES du lac mimo_lean (compilation locale).\")\n",
-    ""
+    "print(\"Sortie ci-dessus : declarations RELLES du lac mimo_lean (compilation locale).\")\n"
    ]
   },
   {
@@ -1261,14 +1260,22 @@
     "tags": []
    },
    "source": [
-    "## Code 3.2 -- NormTails : six declarations et verification Monte-Carlo de la queue\n",
+    "## Code 3.2 -- NormTails : la borne de concentration et sa confrontation Monte-Carlo\n",
     "\n",
-    "Cette cellule `#check` les six déclarations du module `NormTails` du lac, qui\n",
-    "sont les briques de concentration de la norme du bruit, puis vérifie\n",
-    "Monte-Carlo que la borne `noise_norm_tail : P(‖w‖ ≥ t) ≤ exp(−Mt²/2)` tient\n",
-    "sur la queue empirique d'un vecteur gaussien standard de dimension `M = 200`.\n",
+    "Les six déclarations du module `NormTails` ont été interrogées en Code 2.5 :\n",
+    "leurs signatures réelles y sont imprimées par `#check` (du certificat Lipschitz\n",
+    "`Mimo.norm_lipschitz_one` aux queues `Mimo.noise_norm_tail` et\n",
+    "`Mimo.column_norm_tail`). La cellule qui suit ne ré-exécute pas Lean : elle\n",
+    "confronte **numériquement** la borne formelle à une expérience Monte-Carlo.\n",
     "\n",
-    "**Snippet** :\n",
+    "**La borne réellement prouvée** (signature imprimée par le lac) est une\n",
+    "concentration **bilatérale autour de l'espérance**, sans dimension dans\n",
+    "l'exposant : `Mimo.noise_norm_tail` établit `P(|‖w‖ − E‖w‖| ≥ t) ≤ 2·exp(−t²/2)`\n",
+    "pour `w ~ N(0, I_M)` — l'écart de la norme à sa moyenne, pas la norme\n",
+    "elle-même, avec une constante **indépendante de M**. C'est cette forme qui\n",
+    "rend l'union bound du seuil `2 log N` du Théorème 2.1 vectoriel.\n",
+    "\n",
+    "**Rappel du snippet exécuté en Code 2.5** :\n",
     "\n",
     "```lean\n",
     "import NormTails\n",
@@ -1285,16 +1292,15 @@
     "#check Mimo.column_norm_tail\n",
     "```\n",
     "\n",
-    "**Vérification Monte-Carlo** (200 dimensions, 50 000 tirages) : pour `t` dans\n",
-    "`[0.5, 2.5]`, on compare `P_empirique = (‖w‖ ≥ t)` à la borne prouvée\n",
-    "`exp(−Mt²/2)`. La borne est un **upper bound** sur la queue : on attend\n",
-    "`P_emp / borne ≤ 1` pour tout `t`, et un ratio qui **plafonne** sous 1 quand\n",
-    "`M` croît (concentration gaussienne en action). C'est la forme directement\n",
-    "exploitée par l'union bound du seuil `2 log N` du Théorème 2.1.\n",
+    "**Confrontation Monte-Carlo** (50 000 tirages, `M ∈ {50, 200, 1000}`) : pour\n",
+    "`t` dans `[0.5, 3.0]`, on mesure `P_emp = P(|‖w‖ − E‖w‖| > t)` et on la\n",
+    "compare à la borne `2·exp(−t²/2)`. Le ratio mesuré reste `≤ 1` pour tout `t`\n",
+    "et plafonne à ~0,27 — **stable quand M varie** : la concentration autour de la\n",
+    "moyenne est un phénomène sans dimension, exactement ce que dit le théorème.\n",
     "\n",
-    "**Statut de la cellule** : les six `#check` impriment leurs signatures ; la\n",
-    "vérification Monte-Carlo illustre visuellement la borne sur la queue empirique.\n",
-    "L'exécution complète requiert le lac `mimo_lean` compilé localement (Code 2.1)."
+    "**Statut de la cellule suivante** : implémentation pure numpy, sans Lean ni\n",
+    "lac local — les signatures sont celles de Code 2.5, la confrontation est\n",
+    "autonome."
    ]
   },
   {
@@ -1835,21 +1841,26 @@
    "source": [
     "### Exercice 4 : verifier la borne `noise_norm_tail` numeriquement\n",
     "\n",
-    "La cellule Code 3.2 ci-dessus affirme que `noise_norm_tail : P(‖w‖ ≥ t) ≤\n",
-    "exp(−Mt²/2)` pour `w ~ N(0, I_M)`. C'est la brique qui rend l'union bound du\n",
-    "seuil `2 log N` vectorielle et non plus seulement par coordonnee. L'exercice\n",
-    "consiste a **reproduire numeriquement** la verification : pour `M = 200`,\n",
+    "La cellule Code 3.2 ci-dessus confronte `noise_norm_tail` : `P(|‖w‖ − E‖w‖| ≥ t) ≤\n",
+    "2·exp(−t²/2)` pour `w ~ N(0, I_M)`. C'est la brique qui rend l'union bound du\n",
+    "seuil `2 log N` vectoriel et non plus seulement par coordonnee — et sa\n",
+    "caractéristique clé est la constante **sans dimension**. L'exercice\n",
+    "consiste a **reproduire numeriquement** la confrontation : pour `M = 200`,\n",
     "tirer `50 000` vecteurs gaussiens standard, mesurer la queue empirique\n",
-    "`P_emp = (‖w‖ ≥ t)` sur une grille `t ∈ [0.5, 2.5]`, et tracer le ratio\n",
-    "`r(t) = P_emp / exp(−Mt²/2)`. On attend `r(t) ≤ 1` pour tout `t` (la borne\n",
-    "est un upper bound), et `r(t)` qui **plafonne** sous 1 quand `M` augmente\n",
-    "(la concentration gaussienne se manifeste).\n",
+    "`P_emp = P(|‖w‖ − E‖w‖| > t)` sur une grille `t ∈ [0.5, 2.5]`, et tracer le\n",
+    "ratio `r(t) = P_emp / (2·exp(−t²/2))`. On attend `r(t) ≤ 1` pour tout `t`\n",
+    "(la borne est un upper bound).\n",
+    "\n",
+    "**Aller plus loin (le vrai contenu du théorème)** : répéter pour\n",
+    "`M ∈ [50, 100, 200, 400]` et observer que le ratio reste **du même ordre**\n",
+    "quand M croît. `‖w‖` lui-même croît comme `√M`, mais son écart à sa moyenne\n",
+    "reste d'ordre constant — c'est exactement l'échelle que capture la borne sans\n",
+    "dimension, et la raison pour laquelle elle n'est pas perdante.\n",
     "\n",
     "**Indices** : `rng = np.random.default_rng(M)` pour reproductibilite ;\n",
-    "`np.linalg.norm(w, axis=1)` pour la norme par vecteur ; un seul plot\n",
-    "`ax.plot(t, ratio)` en semilog si le ratio varie sur plusieurs ordres.\n",
-    "On peut aussi tester `M ∈ [50, 100, 200, 400]` et observer le ratio chuter\n",
-    "vers 0.5 a mesure que `M` croit (concentration des mesures gaussiennes)."
+    "`np.linalg.norm(w, axis=1)` pour la norme par vecteur ; `E‖w‖` s'estime par\n",
+    "la moyenne empirique des normes ; un seul plot `ax.plot(t, ratio)` — le ratio\n",
+    "reste dans `[0, 1]`, pas besoin d'echelle log."
    ]
   },
   {