From 820cca7c031d4f88cd9cda6ea3d697c1c677b823 Mon Sep 17 00:00:00 2001
From: Remy Degenne <remydegenne@gmail.com>
Date: Tue, 13 Oct 2026 15:33:10 +0200
Subject: [PATCH] bump

---
 .../Online/Bandit/RewardByCountMeasure.lean      |  2 +-
 lake-manifest.json                               | 16 ++++++++--------
 lakefile.toml                                    |  4 ++--
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
index fe804ee9..f7712ec1 100644
--- a/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
+++ b/LeanMachineLearning/Online/Bandit/RewardByCountMeasure.lean
@@ -34,7 +34,7 @@ notation "𝓛[" Y " | " X " in " s "; " μ "]" => Measure.map Y (μ[|X ⁻¹' s
 notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' {x}])
 
 omit [DecidableEq 𝓐] in
-lemma condDistrib_reward'' [Countable 𝓐]
+lemma condDistrib_reward''
     (h : IsAlgEnvSeq O A R alg (stationaryEnv ν) P) (n : ℕ) :
     𝓛[fun ω ↦ R n ω.1 | fun ω ↦ A n ω.1; 𝔓] =ᵐ[(𝔓).map (fun ω ↦ A n ω.1)] ν := by
   have hA := h.measurable_action
diff --git a/lake-manifest.json b/lake-manifest.json
index fb1b62d4..53ea4d70 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1f414401f69059aa7eead47b53ee40bd38455eeb",
+   "rev": "41d048456026a1e519fbc9f74b3734eccc4c8556",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "1f414401f69059aa7eead47b53ee40bd38455eeb",
+   "inputRev": "41d048456026a1e519fbc9f74b3734eccc4c8556",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8fc7a297f14d5adc1a551b5b4ecf283c08bd691f",
+   "rev": "01a09f320122475119588526857a07d218aef600",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.35.0-rc3",
+   "inputRev": "v4.35.0-rc4",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "579f558774c4ac6840e715ba60dabf3030619349",
+   "rev": "80a81552bef492cc13d69cc7abddb61c29abbba3",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b71aaf60877e673fdb921f06f20987d12ee8a290",
+   "rev": "9bfcda9fca2e9438b8a77b6e61e5880f69a82540",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "af451aaa73d8f8025189f228642b6e4fe047ce4f",
+   "rev": "86aa7e62f42b2a82daf9692b191febde1f3d65f9",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -125,7 +125,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d047cb484b2f3598187450935dbcc84d078cb581",
+   "rev": "892d6dc520270b5fb8c1291dd1b131e8c16255ed",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.toml b/lakefile.toml
index 503f44f3..3087673b 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -12,12 +12,12 @@ weak.linter.mathlibStandardSet = true
 [[require]]
 name = "verso"
 git = "https://github.com/leanprover/verso"
-rev = "v4.35.0-rc3"
+rev = "v4.35.0-rc4"
 
 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
-rev = "1f414401f69059aa7eead47b53ee40bd38455eeb"
+rev = "41d048456026a1e519fbc9f74b3734eccc4c8556"
 
 [[lean_lib]]
 name = "LeanMachineLearning"