diff --git a/MyIA.AI.Notebooks/Probas/README.md b/MyIA.AI.Notebooks/Probas/README.md index 4f89778fdb..8094db66b9 100644 --- a/MyIA.AI.Notebooks/Probas/README.md +++ b/MyIA.AI.Notebooks/Probas/README.md @@ -639,7 +639,7 @@ Cette série ancre mathématiquement ses résultats phares dans un assistant de | Probas (DecisionTheory) | `decision_theory_lean` | Coherence utility ⟹ preferences (loterie de référence) (`0 sorry`) | [`DecisionTheory/DecInfer/`](DecisionTheory/DecInfer/README.md) Coherence | | ML ↔ Probas (PAC Learning) | [`learning_theory_lean`](../ML/learning_theory_lean/) | `pac_finite_class_bound` + `pac_agnostic_generalization` (`0 sorry bout-en-bout`) | [`2.8-Theorie-PAC`](../ML/DataScienceWithAgents/02-ML-Cours/2.8-Theorie-PAC.html) + [`2.8b-Theorie-PAC-Lean`](../ML/DataScienceWithAgents/02-ML-Cours/2.8b-Theorie-PAC-Lean.html) | | Probas (DecisionTheory) | `decision_theory_lean` Peters | Indice de Gittins, identités d'escompte (`0 sorry`, ref `v4.27.0-rc1`) | [`DecInfer-08b-Lean-Gittins`](DecisionTheory/DecInfer/DecInfer-08b-Lean-Gittins.ipynb) | -| QC ↔ Probas | `kelly_lean` | Fraction risquée `f* = μ−σ²/2` sous log-bienveillance (`0 sorry`) | [`Kelly_companion.ipynb`](../QuantConnect/kelly_lean/Kelly_companion.ipynb) | +| QC ↔ Probas | `kelly_lean` | Fraction risquée `f* = μ−σ²/2` sous log-bienveillance (`0 sorry`) | [`Kelly_companion-Python.ipynb`](../QuantConnect/kelly_lean/Kelly_companion-Python.html) | | GameTheory ↔ Probas | `game_theory_lean` (Arrow) | Impossibilité d'Arrow (5 axiomes ⇒ dictature) | [`01-Arrow-Impossibility-Theorem.ipynb`](../GameTheory/SocialChoice/01-Arrow-Impossibility-Theorem.ipynb) | | Search ↔ Probas | `search_lean` | Consistance heuristique `h ≤ h*` ⇒ optimalité `A*` | hub Search (cf [`search_lean/`](../Search/search_lean/)) | | SymbolicAI ↔ Probas | `argumentation_lean` | Extension Dung (`grounded`/`preferred`/`stable`) par cadre formel | [`Argumentation-03-Dung-AF-Semantics-Python.ipynb`](../SymbolicAI/Argument_Analysis/Argumentation-03-Dung-AF-Semantics-Python.ipynb) | diff --git a/MyIA.AI.Notebooks/QuantConnect/LEAN_INVENTORY.md b/MyIA.AI.Notebooks/QuantConnect/LEAN_INVENTORY.md index bccf9ef599..619d9202f9 100644 --- a/MyIA.AI.Notebooks/QuantConnect/LEAN_INVENTORY.md +++ b/MyIA.AI.Notebooks/QuantConnect/LEAN_INVENTORY.md @@ -36,5 +36,5 @@ fraction (`kellyFrac_feasible`), et formalisation du pari équivalent (`q`, `pq_ **Câblage CI** : matrice [`lean-ci-matrix.yml`](../../.github/workflows/lean-ci-matrix.yml) (clé `kelly` dans `scripts/lean/ci_lakes.json` ; push `main`, paths `MyIA.AI.Notebooks/QuantConnect/kelly_lean/**.lean` + `lakefile.*`), pipeline `real`. -**Notebooks dans le lake (2, C.2 OK)** : `Kelly_companion.ipynb` (Python) et -`Kelly_companion_lean.ipynb` (Lean) à la racine du lake. +**Notebooks dans le lake (2, C.2 OK)** : `Kelly_companion-Python.ipynb` (Python) et +`Kelly_companion-Lean.ipynb` (Lean) à la racine du lake. diff --git a/MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion_lean.ipynb b/MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Lean.ipynb similarity index 99% rename from MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion_lean.ipynb rename to MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Lean.ipynb index 1f1ff40897..8de58a7f60 100644 --- a/MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion_lean.ipynb +++ b/MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Lean.ipynb @@ -7,7 +7,7 @@ "source": [ "# Kelly — compagnon natif (kernel Lean 4)\n", "\n", - "Ce notebook est le **jumeau à kernel Lean** du compagnon Python `Kelly_companion.ipynb`.\n", + "Ce notebook est le **jumeau à kernel Lean** du compagnon Python `Kelly_companion-Python.ipynb`.\n", "Il rend visible ce que le lake `kelly_lean` **prouve** : chaque énoncé du lake est\n", "importé et vérifié **par le noyau Lean lui-même** (`#check`, `#print axioms`, exemples\n", "re-prouvés en cellule), pas recopié en prose. Le compagnon Python garde la narration\n", @@ -1215,7 +1215,7 @@ "- la version **faisceautique** / multi-pas en temps continu (formalisme de\n", " croissance optimale continue, cf. la littérature Merton).\n", "\n", - "Le compagnon Python (`Kelly_companion.ipynb`) montre quantitativement le premier point :\n", + "Le compagnon Python (`Kelly_companion-Python.ipynb`) montre quantitativement le premier point :\n", "trajectoires composées, ruine du surenchérisseur, effet du demi-Kelly sur les\n", "drawdowns." ] diff --git a/MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion.ipynb b/MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Python.ipynb similarity index 99% rename from MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion.ipynb rename to MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Python.ipynb index 56f3e14d35..9d040c374c 100644 --- a/MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion.ipynb +++ b/MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Python.ipynb @@ -5,7 +5,7 @@ "id": "a95da734", "metadata": {}, "source": [ - "# Le critere de Kelly — compagnon Python du lake `kelly_lean`\n", + "# Kelly — compagnon Python du lake `kelly_lean`\n", "\n", "Ce notebook est le **volet numérique** de la preuve formelle\n", "[`kelly_lean`](./Kelly/Kelly.lean) (Lean 4 + Mathlib). Il montre, cote a cote\n", diff --git a/MyIA.AI.Notebooks/QuantConnect/kelly_lean/README.md b/MyIA.AI.Notebooks/QuantConnect/kelly_lean/README.md index 3652ae610e..6883a019e3 100644 --- a/MyIA.AI.Notebooks/QuantConnect/kelly_lean/README.md +++ b/MyIA.AI.Notebooks/QuantConnect/kelly_lean/README.md @@ -128,5 +128,20 @@ lakes frères) ; deux notebooks compagnons le rendent pédagogique : | Notebook | Rôle | |---|---| -| [`Kelly_companion.ipynb`](Kelly_companion.ipynb) | **Volet numérique (Python)** : montre, côte à côte avec les théorèmes prouvés, pourquoi `f*` maximise le taux de croissance espéré `g(f)` et pourquoi tout sur-pari (`f > f*`) ou sous-pari (`f < f*`) est strictement sous-optimal — narration économique, figures et lien trading. | -| [`Kelly_companion_lean.ipynb`](Kelly_companion_lean.ipynb) | **Jumeau à kernel Lean 4** : chaque énoncé du lake est importé et vérifié par le noyau Lean lui-même (`#check`, `#print axioms`, exemples re-prouvés en cellule) — les énoncés qui compilent, pas la prose recopiée. | +| [`Kelly_companion-Python.ipynb`](Kelly_companion-Python.html) | **Volet numérique (Python)** : montre, côte à côte avec les théorèmes prouvés, pourquoi `f*` maximise le taux de croissance espéré `g(f)` et pourquoi tout sur-pari (`f > f*`) ou sous-pari (`f < f*`) est strictement sous-optimal — narration économique, figures et lien trading. | +| [`Kelly_companion-Lean.ipynb`](Kelly_companion-Lean.html) | **Jumeau à kernel Lean 4** : chaque énoncé du lake est importé et vérifié par le noyau Lean lui-même (`#check`, `#print axioms`, exemples re-prouvés en cellule) — les énoncés qui compilent, pas la prose recopiée. | + +## Carnets suivants + +Plan de croissance trace dans l'issue +[#19516](https://github.com/jsboige/CoursIA/issues/19516) (table postee sur +[#16231](https://github.com/jsboige/CoursIA/issues/16231)) : + +1. **Fractional Kelly mesure** — module Lean `Fractional` (`growth(c*f*) ≤ growth(f*)`, + egalite seulement pour `c = 1`) + companion Python : surface croissance/variance + sur la fraction, multi-seed — la reponse chiffree au « pourquoi demi-Kelly ». +2. **Erreur d'estimation : biais de l'optimiste** — companion Python : + `kellyFrac(p_hat)` applique a `p_hat` bruite → surexposition moyenne mesuree. +3. **Kelly multi-issue** — generalisation de `Bet` a `n` issues (lake) + companion. +4. **Cotes dynamiques / sequence** — companion Python seul (bookmaker qui ajuste + `b_t` dans le temps ; hors lake). diff --git a/_quarto.yml b/_quarto.yml index 4bc18cddb7..08db9e0868 100644 --- a/_quarto.yml +++ b/_quarto.yml @@ -1406,8 +1406,8 @@ project: - "MyIA.AI.Notebooks/Probas/PyMC/PyMC-18-Change-Point.ipynb" - "MyIA.AI.Notebooks/Probas/PyMC/PyMC-19-Survival-Analysis.ipynb" - "MyIA.AI.Notebooks/Probas/PyMC/PyMC-Observabilite-OTel.ipynb" - - "MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion.ipynb" - - "MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion_lean.ipynb" + - "MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Python.ipynb" + - "MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Lean.ipynb" - "MyIA.AI.Notebooks/QuantConnect/ML-Training-Pipeline/c1330_xrp_dt_foldwise_research.ipynb" - "MyIA.AI.Notebooks/QuantConnect/ML-Training-Pipeline/c875_hmm_alpha_dm_research.ipynb" - "MyIA.AI.Notebooks/QuantConnect/ML-Training-Pipeline/hmm_alpha_research.ipynb" diff --git a/docs/curriculum/trading.md b/docs/curriculum/trading.md index 6adf55e147..c76b762e8d 100644 --- a/docs/curriculum/trading.md +++ b/docs/curriculum/trading.md @@ -298,8 +298,8 @@ Stratégies de trading algorithmique avec QuantConnect, pipeline ML (Transformer | # | Notebook | Maturité | Exécutable | |---|----------|----------|------------| -| 1 | [Le critere de Kelly — compagnon Python du lake…](../../MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion.ipynb) | BETA | Non | -| 2 | [Kelly — compagnon natif (kernel Lean 4)](../../MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion_lean.ipynb) | BETA | Non | +| 1 | [Le critere de Kelly — compagnon Python du lake…](../../MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Python.ipynb) | BETA | Non | +| 2 | [Kelly — compagnon natif (kernel Lean 4)](../../MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Lean.ipynb) | BETA | Non | ## QuantConnect/projects (46 notebooks) diff --git a/docs/reference/rename-ledger.tsv b/docs/reference/rename-ledger.tsv index d785295dcb..4b0f5b9422 100644 --- a/docs/reference/rename-ledger.tsv +++ b/docs/reference/rename-ledger.tsv @@ -271,5 +271,7 @@ MyIA.AI.Notebooks/Search/Applications/Hybrid/App-25-CombinatorialAuctions-WDP-VC MyIA.AI.Notebooks/Search/Applications/CSP/App-26-CoveringArrays-Guarantee-Audit.ipynb MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-05-CoveringArrays-Guarantee-Audit-Python.ipynb 2026-10-05 myia-po-2027:CoursIA MyIA.AI.Notebooks/Search/Applications/Hybrid/App-28-LearningToBranch-Generalization-Audit.ipynb MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-06-LearningToBranch-Generalization-Audit-Python.ipynb 2026-10-05 myia-po-2027:CoursIA MyIA.AI.Notebooks/Search/Applications/Hybrid/App-33-NeuralDiving-Coloration.ipynb MyIA.AI.Notebooks/Search/Part5-Frontieres/Frontieres-10-NeuralDiving-Coloration-Python.ipynb 2026-10-05 myia-po-2027:CoursIA +MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion.ipynb MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Python.ipynb 2026-10-06 myia-po-2024:CoursIA +MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion_lean.ipynb MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Lean.ipynb 2026-10-06 myia-po-2024:CoursIA MyIA.AI.Notebooks/RL/rl_17_k_server_wfa.ipynb MyIA.AI.Notebooks/Complexity/Complexity-04c-KServer-WorkFunction-Python.ipynb 2026-10-05 myia-po-2027:CoursIA MyIA.AI.Notebooks/RL/rl_18_matroid_secretary.ipynb MyIA.AI.Notebooks/Complexity/Complexity-04d-Secretaire-Matroidal-Python.ipynb 2026-10-05 myia-po-2027:CoursIA diff --git a/scripts/notebook_tools/pedagogy_density_baseline.json b/scripts/notebook_tools/pedagogy_density_baseline.json index 2e745c4912..9e6f7e44b5 100644 --- a/scripts/notebook_tools/pedagogy_density_baseline.json +++ b/scripts/notebook_tools/pedagogy_density_baseline.json @@ -425,7 +425,7 @@ "MyIA.AI.Notebooks/QuantConnect/Python/QC-Py-Cloud-12-SectorRotation-Momentum.ipynb": 3750.667, "MyIA.AI.Notebooks/QuantConnect/Python/QC-Py-Cloud-14-DualMomentum.ipynb": 3204.333, "MyIA.AI.Notebooks/QuantConnect/Python/QC-Py-Dataset-Workflow.ipynb": 663.071, - "MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion.ipynb": 1125.667, + "MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Python.ipynb": 1125.667, "MyIA.AI.Notebooks/RL/RL-10-Reward-Shaping-Curriculum-Python.ipynb": 1327.5, "MyIA.AI.Notebooks/RL/RL-11-POMDP-Croyances-Python.ipynb": 830.6, "MyIA.AI.Notebooks/RL/RL-12-Distributional-RL-C51-Python.ipynb": 1071.167, diff --git a/scripts/notebook_tools/scan_d2_window_openness.py b/scripts/notebook_tools/scan_d2_window_openness.py index 88329f6c7a..8af4b59017 100644 --- a/scripts/notebook_tools/scan_d2_window_openness.py +++ b/scripts/notebook_tools/scan_d2_window_openness.py @@ -121,7 +121,7 @@ Voir issue #10230 (refutation firsthand de la mesure 82 % de #9772). --- Echantillon D2+ (10 premiers) : - MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion.ipynb + MyIA.AI.Notebooks/QuantConnect/kelly_lean/Kelly_companion-Python.ipynb MyIA.AI.Notebooks/QuantConnect/ML-Training-Pipeline/c875_hmm_alpha_dm_research.ipynb ...