From ecdb0c7ac4b08faa854b2ec172eb575c8e311cd2 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 29 Sep 2025 15:10:16 +0200 Subject: [PATCH 1/4] two pullCount lemmas --- LeanBandits/Regret.lean | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/LeanBandits/Regret.lean b/LeanBandits/Regret.lean index 3dde0476..c0720afe 100644 --- a/LeanBandits/Regret.lean +++ b/LeanBandits/Regret.lean @@ -193,11 +193,24 @@ lemma stepsUntil_eq_congr {h' : ℕ → α × ℝ} (h_eq : ∀ i ≤ n, arm i h lemma pullCount_stepsUntil_add_one (h_exists : ∃ s, pullCount a (s + 1) h = m) : pullCount a (stepsUntil a m h + 1).toNat h = m := by - sorry + classical + have h_eq := stepsUntil_eq_dite a m h + simp only [h_exists, ↓reduceDIte] at h_eq + have h' := Nat.find_spec h_exists + rw [h_eq] + rw [ENat.toNat_add (by simp) (by simp)] + simp only [ENat.toNat_coe, ENat.toNat_one] + exact h' lemma pullCount_stepsUntil (hm : m ≠ 0) (h_exists : ∃ s, pullCount a (s + 1) h = m) : pullCount a (stepsUntil a m h).toNat h = m - 1 := by - sorry + have h_arm := arm_eq_of_stepsUntil_eq_coe (n := (stepsUntil a m h).toNat) (a := a) (ω := h) hm ?_ + swap; · symm; simpa [stepsUntil_eq_top_iff] + have h_add_one := pullCount_stepsUntil_add_one h_exists + nth_rw 1 [← h_arm] at h_add_one + rw [ENat.toNat_add ?_ (by simp), ENat.toNat_one, pullCount_eq_pullCount_add_one] at h_add_one + swap; · simpa [stepsUntil_eq_top_iff] + grind section SumRewards From 29b22b4d58be689ab390a1999b51fb895285ad85 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 29 Sep 2025 16:53:54 +0200 Subject: [PATCH 2/4] Adapted lemmas --- LeanBandits/Algorithm.lean | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/LeanBandits/Algorithm.lean b/LeanBandits/Algorithm.lean index 49c5dc3c..46fb402e 100644 --- a/LeanBandits/Algorithm.lean +++ b/LeanBandits/Algorithm.lean @@ -208,6 +208,43 @@ lemma action_zero_detAlgorithm [MeasurableSingletonClass α] : action 0 =ᵐ[ simp [detAlgorithm] exact ae_of_ae_map (by fun_prop) h_eq +lemma action_eq_eval_comp_hist (n : ℕ) : + action (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).1) ∘ (hist n) := rfl + +lemma reward_eq_eval_comp_hist (n : ℕ) : + reward (α := α) (R := R) n = (fun x ↦ (x ⟨n, by simp⟩).2) ∘ (hist n) := rfl + +lemma measurable_hist_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (hist n) := by + simp [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe, + measurable_iff_comap_le] + +-- todo: due to the type of `Adapted` and the fact that `Iic n → α × R` depends on `n`, we cannot +-- state that `hist` is adapted. + +lemma measurable_action_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (action n) := by + simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe] + rw [action_eq_eval_comp_hist, measurable_iff_comap_le, ← MeasurableSpace.comap_comp] + refine MeasurableSpace.comap_mono ?_ + rw [← measurable_iff_comap_le] + fun_prop + +lemma adapted_action [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] + [SecondCountableTopology α] [OpensMeasurableSpace α] : + Adapted (Learning.filtration α R) action := + fun n ↦ (measurable_action_filtration n).stronglyMeasurable + +lemma measurable_reward_filtration (n : ℕ) : Measurable[Learning.filtration α R n] (reward n) := by + simp only [Learning.filtration, Filtration.piLE_eq_comap_frestrictLe, ← hist_eq_frestrictLe] + rw [reward_eq_eval_comp_hist, measurable_iff_comap_le, ← MeasurableSpace.comap_comp] + refine MeasurableSpace.comap_mono ?_ + rw [← measurable_iff_comap_le] + fun_prop + +lemma adapted_reward [TopologicalSpace R] [TopologicalSpace.PseudoMetrizableSpace R] + [SecondCountableTopology R] [OpensMeasurableSpace R] : + Adapted (Learning.filtration α R) reward := + fun n ↦ (measurable_reward_filtration n).stronglyMeasurable + lemma action_detAlgorithm_ae_eq [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (n : ℕ) : From 4d3ff3307ad71f5e4794e3ac3b0add76590bb0b7 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Mon, 29 Sep 2025 17:19:42 +0200 Subject: [PATCH 3/4] two indep proofs --- LeanBandits/Bandit.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index feb09b34..7ffdb9b9 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -126,12 +126,13 @@ lemma iIndepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] : sorry lemma iIndepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] : - iIndepFun (fun n ω ↦ ω n) (Bandit.streamMeasure ν) := by - sorry + iIndepFun (fun n ω ↦ ω n) (Bandit.streamMeasure ν) := + iIndepFun_infinitePi (μ := 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 ν) := by - sorry + iIndepFun (fun n ω ↦ ω n a) (Bandit.streamMeasure ν) := + (iIndepFun_eval_streamMeasure' ν).comp (g := fun i ω ↦ ω a) (by fun_prop) lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m : ℕ} {a b : α} (h : n ≠ m ∨ a ≠ b) : From 6122d41027601c3b414d6c9c42a366025035f7c5 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 30 Sep 2025 08:40:56 +0200 Subject: [PATCH 4/4] minor --- LeanBandits/Bandit.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index 7ffdb9b9..28435b1b 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -121,10 +121,6 @@ lemma integral_eval_streamMeasure (ν : Kernel α ℝ) [IsMarkovKernel ν] (n : rw [integral_map (Measurable.aemeasurable (by fun_prop)) (by fun_prop)] _ = (ν a)[id] := by simp [(hasLaw_eval_eval_streamMeasure ν n a).map_eq] -lemma iIndepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] : - iIndepFun (fun (p : ℕ × α) ω ↦ ω p.1 p.2) (Bandit.streamMeasure ν) := by - sorry - lemma iIndepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] : iIndepFun (fun n ω ↦ ω n) (Bandit.streamMeasure ν) := iIndepFun_infinitePi (μ := fun (_ : ℕ) ↦ Measure.infinitePi ν) (Ω := fun _ ↦ α → R) @@ -134,6 +130,11 @@ 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 + lemma indepFun_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] {n m : ℕ} {a b : α} (h : n ≠ m ∨ a ≠ b) : IndepFun (fun ω ↦ ω n a) (fun ω ↦ ω m b) (Bandit.streamMeasure ν) := by