Docs(lean,#24634): les pins Mathlib documentes contredisent les lakefiles (3 lakes)

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₃

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₃

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

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

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
 ```