diff --git a/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount.lean b/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount.lean index 18f7b48b4b..8549c9f15d 100644 --- a/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount.lean +++ b/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount.lean @@ -92,9 +92,9 @@ theorem present_value_constant {γ r : ℝ} (hγ₁ : 0 < γ) (hγ₂ : γ < 1) fermée `∑' n, γ^n = 1/(1-γ)` (`geometric_series_converges`), puis ramener le but à `1/(1-γ₁) ≤ 1/(1-γ₂)`. Comme `γ₁ ≤ γ₂` on a `1-γ₂ ≤ 1-γ₁`, et les deux dénominateurs sont positifs (`γ₂ < 1`), donc `one_div_le_one_div_of_le` clôt le - but. Cela contourne l'absence de `tsum_le_tsum` sur `ℝ` (non disponible dans - Mathlib v4.30.0-rc2 pour les séries sur `ℝ` brut) en exploitant la forme - fermée. -/ + but. Cela contourne l'absence de `tsum_le_tsum` sur `ℝ` (non disponible dans la + version alors utilisée, Mathlib v4.30.0-rc2, pour les séries sur `ℝ` brut) en + exploitant la forme fermée. -/ theorem discount_monotone {γ₁ γ₂ : ℝ} (h₁ : 0 ≤ γ₁) (h₂ : γ₁ ≤ γ₂) (h₃ : γ₂ < 1) : ∑' n : ℕ, γ₁ ^ n ≤ ∑' n : ℕ, γ₂ ^ n := by have hγ₁_lt : γ₁ < 1 := lt_of_le_of_lt h₂ h₃ diff --git a/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount_en.lean b/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount_en.lean index 26a6cdf8e7..b3f5af0a11 100644 --- a/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount_en.lean +++ b/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/Gittins/Discount_en.lean @@ -91,8 +91,8 @@ theorem present_value_constant {γ r : ℝ} (hγ₁ : 0 < γ) (hγ₂ : γ < 1) the goal to `1/(1-γ₁) ≤ 1/(1-γ₂)`. Since `γ₁ ≤ γ₂` we have `1-γ₂ ≤ 1-γ₁`, and both denominators are positive (`γ₂ < 1`), so `one_div_le_one_div_of_le` closes the goal. This sidesteps the missing - `tsum_le_tsum` on `ℝ` (not available in Mathlib v4.30.0-rc2 for bare `ℝ` - series) by exploiting the closed form. -/ + `tsum_le_tsum` on `ℝ` (not available in the version then in use, Mathlib + v4.30.0-rc2, for bare `ℝ` series) by exploiting the closed form. -/ theorem discount_monotone {γ₁ γ₂ : ℝ} (h₁ : 0 ≤ γ₁) (h₂ : γ₁ ≤ γ₂) (h₃ : γ₂ < 1) : ∑' n : ℕ, γ₁ ^ n ≤ ∑' n : ℕ, γ₂ ^ n := by have hγ₁_lt : γ₁ < 1 := lt_of_le_of_lt h₂ h₃ diff --git a/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/README.md b/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/README.md index a66123be99..f9331c1384 100644 --- a/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/README.md +++ b/MyIA.AI.Notebooks/Probas/DecisionTheory/decision_theory_lean/README.md @@ -39,7 +39,7 @@ Notebook compagnon Lean : ## Statut -- **Toolchain** : `leanprover/lean4:v4.31.0-rc1` +- **Toolchain** : `leanprover/lean4:v4.33.0` - **Sorry** : **2** (tous dans `gittins_optimality`, `Gittins/GittinsTheorem.lean`) — voir « État honnête » ci-dessous. `Gittins/Discount.lean` = **0 sorry** (entièrement prouvé), `Gittins/Basic.lean` = 0. `gittins_index_known_arm` et @@ -52,7 +52,7 @@ Notebook compagnon Lean : fidèlement — d'où le total lake standalone-sorry = 4). `Utility` et `Coherence` disposent aussi de leurs siblings EN. - **Build** : `lake build Gittins Utility Coherence` (dépend de Mathlib4) -- **Dépendances** : Mathlib4 (`v4.31.0-rc1`) — analyse réelle pour les lemmes +- **Dépendances** : Mathlib4 (pin `db584cd6`, toolchain `v4.33.0`) — analyse réelle pour les lemmes d'actualisation, structure ordonnée et affine de `ℝ` pour vNM, théorie des `Finset` / inclusion–exclusion pour la cohérence de de Finetti @@ -72,7 +72,7 @@ La formalisation est scindée en une couche **prouvée** et une couche **énonc `discount_monotone` (γ₁ ≤ γ₂ ⇒ ∑' γ₁^n ≤ ∑' γ₂^n). `discount_monotone` est prouvé **en forme close** via `geometric_series_converges` + `one_div_le_one_div_of_le`, en contournant l'absence de `tsum_le_tsum` sur le `ℝ` - nu dans Mathlib v4.31.0-rc1. + nu dans la version de Mathlib alors utilisée (`v4.31.0-rc1`, aujourd'hui `v4.33.0`). - **Énoncé, intractable** (`GittinsTheorem.lean`) : `gittinsIndex` (arrêt optimal), `gittins_optimality` (le théorème central — la politique à indice maximise la récompense actualisée espérée). Les **2 `sorry` résiduels** sont dans l'assemblage de @@ -265,7 +265,8 @@ Une preuve complète de `gittins_optimality` requiert : 3. Une **récurrence sur l'horizon de planification**, et 4. Une **espérance formelle** sur la distribution de récompense. -Mathlib (v4.31.0-rc1) n'a **aucune formalisation de MDP, de bandit ou d'équation de +Dans la version de Mathlib alors utilisée (`v4.31.0-rc1`, aujourd'hui `v4.33.0`), il n'y avait +**aucune formalisation de MDP, de bandit ou d'équation de Bellman**, ni d'API d'espérance mesurée-théorique adaptée ici. Une preuve complète exigerait un volume de définitions support de niveau recherche, au-delà d'une seule PR. Le théorème est donc **énoncé** (avec l'énoncé précis préservé dans diff --git a/MyIA.AI.Notebooks/Search/discrepancy_lean/README.md b/MyIA.AI.Notebooks/Search/discrepancy_lean/README.md index 3246ad9026..3bca539466 100644 --- a/MyIA.AI.Notebooks/Search/discrepancy_lean/README.md +++ b/MyIA.AI.Notebooks/Search/discrepancy_lean/README.md @@ -52,7 +52,7 @@ formalisation Lean 4 tierce de cette preuve existe déjà (voir le réaudit du - **0 `sorry`** ; conjectures = `def ... : Prop` nommées, jamais théorèmes tronqués. - Docstrings **FR-first** (i18n #4980). -- Toolchain `leanprover/lean4:v4.32.1`, Mathlib `v4.32.1` (`520045ab`) — +- Toolchain `leanprover/lean4:v4.33.0`, Mathlib pin `db584cd6d46c92f209a44c0f1c829460d327499d` — aligné sur la cohorte fleet (mutualisation #4363). ## Build diff --git a/MyIA.AI.Notebooks/Search/search_lean/README.md b/MyIA.AI.Notebooks/Search/search_lean/README.md index c3cb904023..dadb08c740 100644 --- a/MyIA.AI.Notebooks/Search/search_lean/README.md +++ b/MyIA.AI.Notebooks/Search/search_lean/README.md @@ -213,7 +213,7 @@ prouvés** ; le module ancre ce qui, lui, se vérifie mécaniquement : ## Construction ```bash -lake exe cache get # récupère les .olean de Mathlib (v4.31.0-rc1) +lake exe cache get # récupère les .olean de Mathlib (pin db584cd6) lake build Astar # build de la librairie ```