diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb index a334d927fa..f8fc6b4206 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-21b-MIMO-Converse-Native.ipynb @@ -725,9 +725,9 @@ "tags": [] }, "source": [ - "**Lecture du lakefile et des modules** (cellule code[0]) :\n", + "**Lecture du lakefile et des modules** (cellule code[0], ouverture de la section 1) :\n", "\n", - "La cellule ci-dessus est un *commentaire* Lean qui simule le contenu du\n", + "La cellule code[0], en ouverture de la section 1, est un *commentaire* Lean qui simule le contenu du\n", "`lakefile.lean`. La structure typique d'un lakefile Lean 4 est :\n", "\n", "```lean\n", @@ -1226,48 +1226,6 @@ "#eval 2 * Float.exp (-(4:Float) ^ 2 / 2)" ] }, - { - "cell_type": "markdown", - "id": "c13", - "metadata": { - "papermill": { - "duration": 0.020719, - "end_time": "2026-09-28T15:22:07.358315+00:00", - "exception": false, - "start_time": "2026-09-28T15:22:07.337596+00:00", - "status": "completed" - }, - "tags": [] - }, - "source": [ - "À 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.\n", - "\n", - "**Trois observations physiques** :\n", - "\n", - "1. **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.\n", - "2. **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.\n", - "3. **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'**un** `hᵢ` 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`.\n", - "\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 quadratique** `wᵀ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.\n", - "\n", - "**L'intuition derrière la stabilité du score de flip** : le score de flip est\n", - "`s·‖hᵢ‖² + √s·⟪hᵢ,w⟫`. Le premier terme est *déterministe* (ne dépend pas du\n", - "bruit). Le second terme est *aléatoire* et est ce qui peut faire « basculer » un\n", - "flip. Or `⟪hᵢ,w⟫ ≤ ‖hᵢ‖·‖w‖` par Cauchy-Schwarz. Si `‖hᵢ‖` et `‖w‖` sont\n", - "*concentrés* autour de leurs moyennes (c'est ce que `NormTails` prouve), alors\n", - "`⟪hᵢ,w⟫` est lui-même concentré. Le score de flip ne peut *s'échapper* que\n", - "lorsque les deux normes s'écartent simultanément — un événement *doublement*\n", - "rare.\n", - "\n", - "**La loi des petits nombres appliquée au score de flip** : la probabilité qu'un\n", - "flip donné « batte » le point de départ est dominée par la queue de\n", - "`‖w‖·‖hᵢ‖`. Quand les deux queues sont indépendantes (cas gaussien), la\n", - "probabilité *combinée* est le produit — d'où une probabilité *extrêmement*\n", - "petite. C'est ce que `Bridge.lean` capture formellement.\n", - "\n", - "**Coût** : pas de cellule code — c'est une interprétation." - ] - }, { "cell_type": "markdown", "id": "b169162a", @@ -1302,9 +1260,34 @@ "\n", "**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.\n", "\n", + "**Lecture physique en une ligne** : À 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.\n", + "\n", "**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`).\n", "\n", - "**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`." + "**Trois observations physiques** :\n", + "\n", + "1. **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.\n", + "2. **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.\n", + "3. **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'**un** `hᵢ` 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`.\n", + "\n", + "**L'intuition derrière la stabilité du score de flip** : le score de flip est\n", + "`s·‖hᵢ‖² + √s·⟪hᵢ,w⟫`. Le premier terme est *déterministe* (ne dépend pas du\n", + "bruit). Le second terme est *aléatoire* et est ce qui peut faire « basculer » un\n", + "flip. Or `⟪hᵢ,w⟫ ≤ ‖hᵢ‖·‖w‖` par Cauchy-Schwarz. Si `‖hᵢ‖` et `‖w‖` sont\n", + "*concentrés* autour de leurs moyennes (c'est ce que `NormTails` prouve), alors\n", + "`⟪hᵢ,w⟫` est lui-même concentré. Le score de flip ne peut *s'échapper* que\n", + "lorsque les deux normes s'écartent simultanément — un événement *doublement*\n", + "rare.\n", + "\n", + "**La loi des petits nombres appliquée au score de flip** : la probabilité qu'un\n", + "flip donné « batte » le point de départ est dominée par la queue de\n", + "`‖w‖·‖hᵢ‖`. Quand les deux queues sont indépendantes (cas gaussien), la\n", + "probabilité *combinée* est le produit — d'où une probabilité *extrêmement*\n", + "petite. C'est ce que `Bridge.lean` capture formellement.\n", + "\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 quadratique** `wᵀ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 — la frontiere entre les deux routes est tracee dans la documentation du module `Converse`.\n", + "\n", + "**Coût** : pas de cellule code — c'est une interprétation." ] }, { @@ -1496,9 +1479,9 @@ "tags": [] }, "source": [ - "**Lecture des théorèmes SLT empruntés** (cellules code[1]–[2]) :\n", + "**Lecture des théorèmes SLT empruntés** (cellules code[1]–[2], section 1.1) :\n", "\n", - "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).\n", + "Les 4 `#check` — exécutés en section 1.1, en tête du carnet — rendent les *signatures* des théorèmes SLT consommés par le lac (les signatures complètes, verbatim, y sont commentées).\n", "\n", "**`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é.\n", "\n", @@ -1872,7 +1855,7 @@ "source": [ "**Lecture de `norm_concentration` et ses axiomes** (cellule code[4]) :\n", "\n", - "La cellule ci-dessus inclut un `#print axioms Mimo.norm_concentration` — un\n", + "La cellule code[4] (section 2, Briques B) inclut un `#print axioms Mimo.norm_concentration` — un\n", "*audit formel* des axiomes utilisés par ce théorème.\n", "\n", "**Résultat attendu** :\n", @@ -1898,7 +1881,7 @@ "`axiom my_special_axiom : True` et ensuite « prouver » n'importe quoi. `#print\n", "axioms` ferme cette porte.\n", "\n", - "**Le `#print axioms Mimo.column_norm_tail`** de la cellule code[5] : même\n", + "**Le `#print axioms Mimo.column_norm_tail`** de la cellule code[5] (section 2, Briques C) : même\n", "audit pour l'instanciation MIMO. Le résultat attendu est identique\n", "(`propext, Classical.choice, Quot.sound`) — ce qui confirme que la\n", "spécialisation MIMO n'introduit pas d'axiome exotique.\n", @@ -2167,6 +2150,47 @@ }, "tags": [] }, + "source": [ + "### Lecture des minorations de la densite gaussienne (ancre sur code[10])\n", + "\n", + "La sortie verbatim de code[10] enumere les declarations. Certaines d'entre elles portent la substance :\n", + "\n", + "```\n", + "open Mimo in\n", + "#check gaussianPDFReal_lower_abs\n", + "─────▶ Mimo.gaussianPDFReal_lower_abs {R x : ℝ} (hx : |x| ≤ R) :\n", + " Real.exp (-R ^ 2 / 2) / √(2 * Real.pi) ≤ ProbabilityTheory.gaussianPDFReal 0 1 x\n", + "#check one_sub_pow_le_exp_mul\n", + "─────▶ Mimo.one_sub_pow_le_exp_mul {n : ℕ} {p : ℝ} (hn : 0 < n) (hp0 : 0 ≤ p) (hp : p ≤ 1) :\n", + " (1 - p) ^ n ≤ Real.exp (-(↑n * p))\n", + "```\n", + "\n", + "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.\n", + "\n", + "**Trois roles** :\n", + "\n", + "1. **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.\n", + "2. **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π)`.\n", + "3. **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` evite le cas degenere `n = 0`, ou les deux membres valent `1` (egalite triviale, qui ne porte aucune information) : elle garantit que la minoration a un contenu.\n", + "\n", + "**Composition dans le lake** : ces briques se retrouvent dans la borne `ml_error_prob_ge_threshold` (cf. section 4, `ml_error_prob_ge_threshold`), 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.\n", + "\n", + "**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 section 2.1)." + ] + }, + { + "cell_type": "markdown", + "id": "b500bc33", + "metadata": { + "papermill": { + "duration": 0.052452, + "end_time": "2026-09-28T15:22:08.992786+00:00", + "exception": false, + "start_time": "2026-09-28T15:22:08.940334+00:00", + "status": "completed" + }, + "tags": [] + }, "source": [ "## 4. `Bridge` — ce que le converse dit du décodeur ML\n", "\n", @@ -2223,47 +2247,6 @@ "**Le théorème final de `Bridge`** : `ml_error_prob_ge_threshold` *minore* 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." ] }, - { - "cell_type": "markdown", - "id": "b500bc33", - "metadata": { - "papermill": { - "duration": 0.052452, - "end_time": "2026-09-28T15:22:08.992786+00:00", - "exception": false, - "start_time": "2026-09-28T15:22:08.940334+00:00", - "status": "completed" - }, - "tags": [] - }, - "source": [ - "### Lecture des minorations de la densite gaussienne (ancre sur code[10])\n", - "\n", - "La sortie verbatim de code[10] enumere les declarations. Certaines d'entre elles portent la substance :\n", - "\n", - "```\n", - "open Mimo in\n", - "#check gaussianPDFReal_lower_abs\n", - "─────▶ Mimo.gaussianPDFReal_lower_abs {R x : ℝ} (hx : |x| ≤ R) :\n", - " Real.exp (-R ^ 2 / 2) / √(2 * Real.pi) ≤ ProbabilityTheory.gaussianPDFReal 0 1 x\n", - "#check one_sub_pow_le_exp_mul\n", - "─────▶ Mimo.one_sub_pow_le_exp_mul {n : ℕ} {p : ℝ} (hn : 0 < n) (hp0 : 0 ≤ p) (hp : p ≤ 1) :\n", - " (1 - p) ^ n ≤ Real.exp (-(↑n * p))\n", - "```\n", - "\n", - "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.\n", - "\n", - "**Trois roles** :\n", - "\n", - "1. **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.\n", - "2. **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π)`.\n", - "3. **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.\n", - "\n", - "**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.\n", - "\n", - "**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])." - ] - }, { "cell_type": "code", "execution_count": 12,