Update Mathlib

.github/workflows/blueprint.yml

@@ -42,7 +42,7 @@ jobs:
         run: env LEAN_ABORT_ON_PANIC=1 ~/.elan/bin/lake exe runLinter LeanBandits
 
       - name: Compile blueprint and documentation
-        uses: leanprover-community/docgen-action@095763bcfa35bef9c6a3eb8ae778c5e6c7727df2 # 2025-07-03
+        uses: leanprover-community/docgen-action@1417dc7f90338c875da5e5870c03a287d8348896 # docgen-action#11
         with:
           blueprint: true
           homepage: home_page

LeanBandits/Bandit/Bandit.lean

@@ -48,9 +48,12 @@ deriving IsProbabilityMeasure
 
 /-- Measure of an infinite stream of rewards from each arm. -/
 noncomputable
-def streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] : Measure (ℕ → α → R) :=
+def streamMeasure (ν : Kernel α R) : Measure (ℕ → α → R) :=
   Measure.infinitePi fun _ ↦ Measure.infinitePi ν
-deriving IsProbabilityMeasure
+
+instance (ν : Kernel α R) [IsMarkovKernel ν] : IsProbabilityMeasure (streamMeasure ν) := by
+  unfold streamMeasure
+  infer_instance
 
 /-- Joint distribution of the sequence of arm pulled and rewards, and a stream of independent
 rewards from all arms. -/
@@ -121,17 +124,16 @@ lemma integral_eval_streamMeasure (ν : Kernel α ℝ) [IsMarkovKernel ν] (n :
 
 lemma iIndepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] :
     iIndepFun (fun n ω ↦ ω n) (Bandit.streamMeasure ν) :=
-  iIndepFun_infinitePi (μ := fun (_ : ℕ) ↦ Measure.infinitePi ν) (Ω := fun _ ↦ α → R)
+  iIndepFun_infinitePi (P := fun (_ : ℕ) ↦ Measure.infinitePi ν) (Ω := fun _ ↦ α → R)
     (X := fun i u ↦ u) (fun i ↦ by fun_prop)
 
 lemma iIndepFun_eval_streamMeasure'' (ν : Kernel α R) [IsMarkovKernel ν] (a : α) :
     iIndepFun (fun n ω ↦ ω n a) (Bandit.streamMeasure ν) :=
   (iIndepFun_eval_streamMeasure' ν).comp (g := fun i ω ↦ ω a) (by fun_prop)
 
 lemma iIndepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] :
-    iIndepFun (fun (p : ℕ × α) ω ↦ ω p.1 p.2) (Bandit.streamMeasure ν) := by
-  have h_ind := iIndepFun_eval_streamMeasure' ν
-  sorry -- essentially done by Etienne in Mathlib PRs
+    iIndepFun (fun (p : ℕ × α) ω ↦ ω p.1 p.2) (Bandit.streamMeasure ν) :=
+  iIndepFun_uncurry_infinitePi' (X := fun _ _ ↦ id) (fun _ ↦ ν) (by fun_prop)
 
 lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m : ℕ} {a b : α}
     (h : n ≠ m ∨ a ≠ b) :
@@ -249,18 +251,16 @@ lemma HasLaw_arm_zero_detAlgorithm : HasLaw (arm 0) (Measure.dirac arm0) 𝔓t w
   map_eq := (hasLaw_arm_zero _ _).map_eq
 
 lemma arm_zero_detAlgorithm [MeasurableSingletonClass α] :
-    arm 0 =ᵐ[𝔓t] fun _ ↦ arm0 := by
-  have h_eq : ∀ᵐ x ∂(((𝔓t).map (arm 0))), x = arm0 := by
-    rw [(hasLaw_arm_zero _ _).map_eq]
-    simp [detAlgorithm]
-  exact ae_of_ae_map (by fun_prop) h_eq
-
-lemma arm_detAlgorithm_ae_eq (n : ℕ) :
-    arm (n + 1) =ᵐ[𝔓t] fun h ↦ nextArm n (fun i ↦ h i) := by
-  -- rhs equals nextArm n ∘ hist n
-  sorry
+    arm 0 =ᵐ[𝔓t] fun _ ↦ arm0 :=
+  Learning.action_zero_detAlgorithm
+
+lemma arm_detAlgorithm_ae_eq [StandardBorelSpace α] [Nonempty α]
+    [StandardBorelSpace R] [Nonempty R] (n : ℕ) :
+    arm (n + 1) =ᵐ[𝔓t] fun h ↦ nextArm n (fun i ↦ h i) :=
+  Learning.action_detAlgorithm_ae_eq n
 
-example [MeasurableSingletonClass α] :
+example [StandardBorelSpace α] [Nonempty α]
+    [StandardBorelSpace R] [Nonempty R] :
     ∀ᵐ h ∂(𝔓t), arm 0 h = arm0 ∧ ∀ n, arm (n + 1) h = nextArm n (fun i ↦ h i) := by
   rw [eventually_and, ae_all_iff]
   exact ⟨arm_zero_detAlgorithm, arm_detAlgorithm_ae_eq⟩

LeanBandits/BanditAlgorithms/ETC.lean

@@ -217,8 +217,12 @@ lemma identDistrib_aux (m : ℕ) (a b : Fin K) :
     have h_eq (ω : (ℕ → Fin K × ℝ) × (ℕ → Fin K → ℝ)) : ∑ s ∈ Icc 1 m, rewardByCount a s ω.1 ω.2
         = ∑ s ∈ range m, rewardByCount a (s + 1) ω.1 ω.2 := by
       let e : Icc 1 m ≃ range m :=
-      { toFun x := ⟨x - 1, by have h := x.2; simp only [mem_Icc] at h; grind⟩
-        invFun x := ⟨x + 1, by have h := x.2; simp only [mem_Icc]; grind⟩
+      { toFun x := ⟨x - 1, by have h := x.2; simp only [mem_Icc] at h; simp; grind⟩
+        invFun x := ⟨x + 1, by
+          have h := x.2
+          simp only [mem_Icc, le_add_iff_nonneg_left, zero_le, true_and, ge_iff_le]
+          simp only [mem_range] at h
+          grind⟩
         left_inv x := by have h := x.2; simp only [mem_Icc] at h; grind
         right_inv x := by have h := x.2; grind }
       rw [← sum_coe_sort (Icc 1 m), ← sum_coe_sort (range m), sum_equiv e]

LeanBandits/SequentialLearning/Deterministic.lean

@@ -44,6 +44,7 @@ lemma action_detAlgorithm_ae_eq
     [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R]
     (n : ℕ) :
     action (n + 1) =ᵐ[𝔓] fun h ↦ nextaction n (fun i ↦ h i) := by
+  -- rhs equals nextAction n ∘ hist n
   have h := condDistrib_action (detAlgorithm nextaction h_next action0) env n
   simp only [detAlgorithm_policy] at h
   sorry

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "be9d1e42709f0c71f23bf54fdcea77c4058cd659",
+   "rev": "21083832f383e338d7dc4d708dd328018610454e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,