Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion MyIA.AI.Notebooks/Probas/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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) |
Expand Down
4 changes: 2 additions & 2 deletions MyIA.AI.Notebooks/QuantConnect/LEAN_INVENTORY.md
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down Expand Up @@ -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."
]
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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",
Expand Down
19 changes: 17 additions & 2 deletions MyIA.AI.Notebooks/QuantConnect/kelly_lean/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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).
4 changes: 2 additions & 2 deletions _quarto.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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"
Expand Down
4 changes: 2 additions & 2 deletions docs/curriculum/trading.md
Original file line number Diff line number Diff line change
Expand Up @@ -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)

Expand Down
2 changes: 2 additions & 0 deletions docs/reference/rename-ledger.tsv
Original file line number Diff line number Diff line change
Expand Up @@ -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
2 changes: 1 addition & 1 deletion scripts/notebook_tools/pedagogy_density_baseline.json
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion scripts/notebook_tools/scan_d2_window_openness.py
Original file line number Diff line number Diff line change
Expand Up @@ -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
...

Expand Down
Loading