chore(prose-counts,#17636): Probas g10-probas — résorption des mesures d'artefact en prose markdown (4 carnets, 11 gestes)

MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-02-Lean-ExpectedUtility.ipynb

@@ -19,7 +19,7 @@
     "(lib `Utility`), qui prouve la **direction sound** du théorème de représentation d'utilité\n",
     "espérée de **von Neumann–Morgenstern** : si une fonction d'utilité `u` *représente* une\n",
     "préférence `P` (`P p q ↔ E_p[u] ≥ E_q[u]`), alors `P` est **rationnelle** (satisfait les\n",
-    "quatre axiomes vNM), avec **zéro `sorry`**.\n",
+    "quatre axiomes vNM), sans `sorry`.\n",
     "\n",
     "La **cohérence de de Finetti** (prix non arbitrage ⟺ bornes de probabilité, lib `Coherence`)\n",
     "a son companion dédié : [DecInfer-02b-Lean-Coherence](DecInfer-02b-Lean-Coherence.ipynb).\n",
@@ -56,8 +56,8 @@
    "source": [
     "## 1. Import des modules `Utility` du lake `decision_theory_lean`\n",
     "\n",
-    "Le lake porte 3 libs indépendantes (`Utility`, `Gittins`, `Coherence`). On importe\n",
-    "**uniquement les 3 modules de `Utility`** (`Basic`, `Axioms`, `Representation`) — la lib\n",
+    "Le lake porte des libs indépendantes (`Utility`, `Gittins`, `Coherence`). On importe\n",
+    "**uniquement les modules de `Utility`** (`Basic`, `Axioms`, `Representation`) — la lib\n",
     "`Utility` est déclarée via `roots := #[`Utility]`, qui ne build **pas** l'umbrella racine\n",
     "`Utility.olean` (on importe donc les modules directement). On évite `Gittins` (sorries\n",
     "HOLD). La lib `Coherence` — également sorry-free — a son companion dédié\n",
@@ -158,7 +158,7 @@
     "\n",
     "Le théorème phare `expected_utility_rep_is_rational` (direction sound : représentation ⟹\n",
     "rationalité) ne dépend que des **3 axiomes standards de Lean** (`propext`, `Classical.choice`,\n",
-    "`Quot.sound`) — pas de `sorryAx` — ce qui prouve que la preuve est **complète** (0 sorry)."
+    "`Quot.sound`) — pas de `sorryAx` — ce qui prouve que la preuve est **complète**."
    ]
   },
   {
@@ -854,7 +854,7 @@
    "source": [
     "## 6. La chaîne causale complète\n",
     "\n",
-    "Les trois modules de la lib `Utility` composent une chaîne unique, des loteries à la rationalité :\n",
+    "Les modules de la lib `Utility` composent une chaîne unique, des loteries à la rationalité :\n",
     "\n",
     "1. **`Basic`** — `Lottery`/`expectation`/`mix` + `expectation_mix`/`expectation_affine` (l'algèbre affine de l'espérance).\n",
     "2. **`Axioms`** — `Pref`/les 4 axiomes/`IsRational` (le cadre de la rationalité).\n",
@@ -997,7 +997,7 @@
    "source": [
     "## Conclusion\n",
     "\n",
-    "Ce companion **natif** exhibe la preuve formelle 0-sorry de la direction sound du\n",
+    "Ce companion **natif** exhibe la preuve formelle sans `sorry` de la direction sound du\n",
     "théorème de représentation d'utilité espérée de von Neumann–Morgenstern dans le kernel\n",
     "Lean lui-même : `#check` et `#print axioms` rendent les signatures et les axiomes réels\n",
     "produits par le compilateur, sans intermédiaire Python.\n",

MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-08-Sequential.ipynb

@@ -4778,7 +4778,7 @@
     "\n",
     "## Fin de la Serie Decision Theory\n",
     "\n",
-    "Felicitations ! Vous avez termine les 7 notebooks sur la Decision Theory.\n",
+    "Felicitations ! Vous avez termine les notebooks sur la Decision Theory.\n",
     "\n",
     "### Recapitulatif de la serie 14-20\n",
     "\n",

MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-09-Lean-Gittins.ipynb

@@ -865,7 +865,7 @@
     "\n",
     "La politique la plus simple : a chaque etape, jouer le bras avec la meilleure moyenne empirique. Le probleme : elle peut se bloquer sur un bras sous-optimal si l'exploration initiale est defavorable.\n",
     "\n",
-    "Cette section est le pivot pedagogique du notebook : jusqu'ici (sections 1-2) on a defini le **cadre** — bandit, somme actualisee, propriete geometrique du facteur d'actualisation. A partir de maintenant, la question change de nature : parmi toutes les strategies jouables, lesquelles sont **prouvablement bonnes** ? La reponse s'obtient en deux temps, et les deux cellules qui suivent les incarnent :\n",
+    "Cette section est le pivot pedagogique du notebook : jusqu'ici (sections 1-2) on a defini le **cadre** — bandit, somme actualisee, propriete geometrique du facteur d'actualisation. A partir de maintenant, la question change de nature : parmi toutes les strategies jouables, lesquelles sont **prouvablement bonnes** ? La reponse s'obtient en deux temps, et les cellules qui suivent les incarnent :\n",
     "\n",
     "1. La cellule greedy formalise la strategie la plus naturelle (exploiter ce qui semble le meilleur) — lisible, mais non optimale ;\n",
     "2. La cellule contre-exemple prouve en Lean **pourquoi** elle echoue : un scenario a 2 bras ou la moyenne empirique apres un tirage ment sur l'ordre reel des bras (0.8 observe contre 0.3 vrai ; 0.2 observe contre 0.7 vrai), et ou le greedy, fige sur cette erreur initiale, ne s'en remet jamais.\n",
@@ -2805,7 +2805,7 @@
     "| Monotonie en gamma | `gittins_index_monotone_gamma` | sorry |\n",
     "| Regret UCB1 | `ucb1_sublinear_regret` | sorry (INTRACTABLE) |\n",
     "\n",
-    "### 7.2 Repertoire des sorry (8 sorry au total : 2 INTRINSIC lake + 6 locaux)\n",
+    "### 7.2 Repertoire des sorry\n",
     "\n",
     "| sorry | Cellule | Raison |\n",
     "|-------|---------|--------|\n",
@@ -2824,7 +2824,7 @@
     "\n",
     "Le projet Lake contient les mêmes definitions avec Mathlib pour les preuves rigoureuses :\n",
     "\n",
-    "- `Discount.lean` : `geometric_series_converges`, `present_value_constant`, `discount_monotone` — tous prouves via Mathlib (0 sorry)\n",
+    "- `Discount.lean` : `geometric_series_converges`, `present_value_constant`, `discount_monotone` — tous prouves via Mathlib\n",
     "- `GittinsTheorem.lean` : `gittinsIndex` (def = `arm.trueMean`, prouve), `gittins_index_known_arm` (prouve par `rfl`), `gittins_beats_greedy` (`trivial`), `gittins_optimality` (sorry — INTRACTABLE : MDP/Bellman absent Mathlib), `gittins_index_monotone_discount` (sorry — barriere FLOAT-ORDER : IEEE 754 sur `Float`, pas d'instance `Preorder`)\n",
     "\n",
     "**Total sorry (lake)** : 0 (Discount) + 2 (GittinsTheorem) = 2 sorry dans le projet Lake\n",

MyIA.AI.Notebooks/Probas/Infer/Infer-15-Recommenders.ipynb

@@ -7970,7 +7970,7 @@
     "\n",
     "## Serie Complete\n",
     "\n",
-    "Felicitations ! Vous avez termine la serie **Programmation Probabiliste avec Infer.NET** (13 notebooks).\n",
+    "Felicitations ! Vous avez termine la serie **Programmation Probabiliste avec Infer.NET**.\n",
     "\n",
     "| # | Notebook | Concepts |\n",
     "|---|----------|----------|\n",

scripts/notebook_tools/twin_pairs.d/probas-15-recommenders/0020-2026-09-29-myia-po-2025-CoursIA.yaml

@@ -0,0 +1,6 @@
+date: '2026-09-29'
+by: myia-po-2025:CoursIA
+python_sha: 70bbf5c991160fa0e83bdca8cf45ec2cb5cd130d
+csharp_sha: bd49f34e54f98b8d08d996787837e5ad8f4850be
+content_python_sha: dfd77f3efe3ae798c1a728d925cf3d728af205bb425cccea551a8be2962a1ed6
+content_csharp_sha: fe193d0258714ebe345b1caa37fa3c8b4c3485c88f5760bf05704f3a39341d88