diff --git a/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-02-Lean-ExpectedUtility.ipynb b/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-02-Lean-ExpectedUtility.ipynb index 412cc30248..8002e2e4d1 100644 --- a/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-02-Lean-ExpectedUtility.ipynb +++ b/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", diff --git a/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-08-Sequential.ipynb b/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-08-Sequential.ipynb index b28bd113bf..3b228f9fec 100644 --- a/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-08-Sequential.ipynb +++ b/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", diff --git a/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-09-Lean-Gittins.ipynb b/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-09-Lean-Gittins.ipynb index 5dab679ada..55bc93e2de 100644 --- a/MyIA.AI.Notebooks/Probas/DecisionTheory/DecInfer/DecInfer-09-Lean-Gittins.ipynb +++ b/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", diff --git a/MyIA.AI.Notebooks/Probas/Infer/Infer-15-Recommenders.ipynb b/MyIA.AI.Notebooks/Probas/Infer/Infer-15-Recommenders.ipynb index 453a42f3c8..bd49f34e54 100644 --- a/MyIA.AI.Notebooks/Probas/Infer/Infer-15-Recommenders.ipynb +++ b/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", diff --git a/scripts/notebook_tools/twin_pairs.d/probas-15-recommenders/0020-2026-09-29-myia-po-2025-CoursIA.yaml b/scripts/notebook_tools/twin_pairs.d/probas-15-recommenders/0020-2026-09-29-myia-po-2025-CoursIA.yaml new file mode 100644 index 0000000000..e34707d050 --- /dev/null +++ b/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