From b877a6e8401410d0fc640feb2cc5c6d1066c51e0 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 25 Oct 2025 13:44:19 +0200 Subject: [PATCH 1/6] remove one sorry --- LeanBandits/Bandit/Bandit.lean | 11 ++++++----- LeanBandits/SequentialLearning/Deterministic.lean | 1 + 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index e109799a..0e78a3d0 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -255,12 +255,13 @@ lemma arm_zero_detAlgorithm [MeasurableSingletonClass α] : 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 +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⟩ diff --git a/LeanBandits/SequentialLearning/Deterministic.lean b/LeanBandits/SequentialLearning/Deterministic.lean index 5a56ffe8..28bf91d9 100644 --- a/LeanBandits/SequentialLearning/Deterministic.lean +++ b/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 From 2d4c22cfb2e7feefa214a571be374141e603d523 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sat, 25 Oct 2025 13:47:17 +0200 Subject: [PATCH 2/6] golf --- LeanBandits/Bandit/Bandit.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index 0e78a3d0..fed72897 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -249,11 +249,8 @@ 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 + arm 0 =ᵐ[𝔓t] fun _ ↦ arm0 := + Learning.action_zero_detAlgorithm lemma arm_detAlgorithm_ae_eq [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (n : ℕ) : From 586837cd5b9fe89fb1278d05f249b39a2a6abce9 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 26 Oct 2025 10:07:49 +0100 Subject: [PATCH 3/6] bump --- LeanBandits/Bandit/Bandit.lean | 2 +- LeanBandits/BanditAlgorithms/ETC.lean | 8 ++++++-- lake-manifest.json | 2 +- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index fed72897..bf920e53 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -121,7 +121,7 @@ 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 : α) : diff --git a/LeanBandits/BanditAlgorithms/ETC.lean b/LeanBandits/BanditAlgorithms/ETC.lean index eecf76f5..3e85e1ce 100644 --- a/LeanBandits/BanditAlgorithms/ETC.lean +++ b/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] diff --git a/lake-manifest.json b/lake-manifest.json index cb6ea687..49a20969 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "be9d1e42709f0c71f23bf54fdcea77c4058cd659", + "rev": "21083832f383e338d7dc4d708dd328018610454e", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null, From 3d835f25587ee2e34964e21623eaec77a101a6a0 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 26 Oct 2025 10:08:19 +0100 Subject: [PATCH 4/6] CI fix --- .github/workflows/blueprint.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/blueprint.yml b/.github/workflows/blueprint.yml index 438de104..2a96e7af 100644 --- a/.github/workflows/blueprint.yml +++ b/.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 From 2e56c5c8d59d973cca0f1faa23fef86bfc421b12 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 26 Oct 2025 10:09:54 +0100 Subject: [PATCH 5/6] prove sorry --- LeanBandits/Bandit/Bandit.lean | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index bf920e53..cf1feceb 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -129,9 +129,8 @@ lemma iIndepFun_eval_streamMeasure'' (ν : Kernel α R) [IsMarkovKernel ν] (a : (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) : From 8b6374add30038205b5a5bd4c6ad9c1551e78d41 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 26 Oct 2025 10:26:24 +0100 Subject: [PATCH 6/6] lint --- LeanBandits/Bandit/Bandit.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index cf1feceb..9192439b 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/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. -/