From 025875b6e7a6a80f2d1ebb9fb2b8cb2e5a57eb2d Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 22 Jan 2026 14:43:14 +0100 Subject: [PATCH 1/5] add round-robin alg; add isAlgEnvSeqUntil --- LeanBandits.lean | 1 + LeanBandits/BanditAlgorithms/RoundRobin.lean | 91 +++++++++++++++++++ LeanBandits/ForMathlib/Traj.lean | 30 +++++- LeanBandits/SequentialLearning/Algorithm.lean | 51 ++++++++++- 4 files changed, 166 insertions(+), 7 deletions(-) create mode 100644 LeanBandits/BanditAlgorithms/RoundRobin.lean diff --git a/LeanBandits.lean b/LeanBandits.lean index c1a8f31c..4ded5a54 100644 --- a/LeanBandits.lean +++ b/LeanBandits.lean @@ -4,6 +4,7 @@ import LeanBandits.Bandit.RewardByCountMeasure import LeanBandits.Bandit.SumRewards import LeanBandits.BanditAlgorithms.AuxSums import LeanBandits.BanditAlgorithms.ETC +import LeanBandits.BanditAlgorithms.RoundRobin import LeanBandits.BanditAlgorithms.UCB import LeanBandits.ForMathlib.CondDistrib import LeanBandits.ForMathlib.CondIndepFun diff --git a/LeanBandits/BanditAlgorithms/RoundRobin.lean b/LeanBandits/BanditAlgorithms/RoundRobin.lean new file mode 100644 index 00000000..e8021c60 --- /dev/null +++ b/LeanBandits/BanditAlgorithms/RoundRobin.lean @@ -0,0 +1,91 @@ +/- +Copyright (c) 2025 Rémy Degenne. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Rémy Degenne +-/ +import LeanBandits.Bandit.SumRewards +import LeanBandits.BanditAlgorithms.AuxSums +import LeanBandits.ForMathlib.MeasurableArgMax +import LeanBandits.SequentialLearning.Deterministic + +/-! # Round-Robin algorithm + +That algorithm pulls each arm in a round-robin fashion. + +-/ + +open MeasureTheory ProbabilityTheory Finset Learning +open scoped ENNReal NNReal + +namespace Bandits + +variable {K : ℕ} + +section AlgorithmDefinition + +/-- Arm pulled by the Round-Robin algorithm at time `n + 1`. This is arm `n % K`. -/ +noncomputable +def RoundRobin.nextArm (hK : 0 < K) (n : ℕ) (_h : Iic n → Fin K × ℝ) : Fin K := + ⟨(n + 1) % K, Nat.mod_lt _ hK⟩ -- for `n = 0` we have pulled arm 0 already, and we pull arm 1 + +/-- The next arm pulled by Round-Robin is chosen in a measurable way. -/ +@[fun_prop] +lemma RoundRobin.measurable_nextArm (hK : 0 < K) (n : ℕ) : Measurable (nextArm hK n) := by + unfold nextArm + fun_prop + +/-- The Round-Robin algorithm: deterministic algorithm that chooses the next arm according +to `RoundRobin.nextArm`. -/ +noncomputable +def roundRobinAlgorithm (hK : 0 < K) : Algorithm (Fin K) ℝ := + detAlgorithm (RoundRobin.nextArm hK) (by fun_prop) ⟨0, hK⟩ + +end AlgorithmDefinition + +namespace RoundRobin + +variable {hK : 0 < K} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν] + {Ω : Type*} {mΩ : MeasurableSpace Ω} + {P : Measure Ω} [IsProbabilityMeasure P] + {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} + +lemma arm_zero [Nonempty (Fin K)] + (h : IsAlgEnvSeq A R (roundRobinAlgorithm hK) (stationaryEnv ν) P) : + A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ := by + have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK + exact h.action_zero_detAlgorithm + +lemma arm_ae_eq_roundRobinNextArm [Nonempty (Fin K)] + (h : IsAlgEnvSeq A R (roundRobinAlgorithm hK) (stationaryEnv ν) P) (n : ℕ) : + A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK n (IsAlgEnvSeq.hist A R n ω) := by + have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK + exact h.action_detAlgorithm_ae_eq n + +/-- The arm pulled at time `n` is the arm `n % K`. -/ +lemma arm_ae_eq [Nonempty (Fin K)] + (h : IsAlgEnvSeq A R (roundRobinAlgorithm hK) (stationaryEnv ν) P) (n : ℕ) : + A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := by + cases n with + | zero => exact arm_zero h + | succ n => + filter_upwards [arm_ae_eq_roundRobinNextArm h n] with h hn_eq + rw [hn_eq, nextArm] + +/-- At time `K * m`, the number of pulls of each arm is equal to `m`. -/ +lemma pullCount_mul [Nonempty (Fin K)] + (h : IsAlgEnvSeq A R (roundRobinAlgorithm hK) (stationaryEnv ν) P) (a : Fin K) (m : ℕ) : + pullCount A a (K * m) =ᵐ[P] fun _ ↦ m := by + rw [Filter.EventuallyEq] + simp_rw [pullCount_eq_sum] + have h_arm (n : range (K * m)) : A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := arm_ae_eq h n + simp_rw [Filter.EventuallyEq, ← ae_all_iff] at h_arm + filter_upwards [h_arm] with ω h_arm + have h_arm' {i : ℕ} (hi : i ∈ range (K * m)) : A i ω = ⟨i % K, Nat.mod_lt _ hK⟩ := h_arm ⟨i, hi⟩ + calc (∑ s ∈ range (K * m), if A s ω = a then 1 else 0) + _ = (∑ s ∈ range (K * m), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := + sum_congr rfl fun s hs ↦ by rw [h_arm' hs] + _ = m := sum_mod_range_mul hK m a + +end RoundRobin + +end Bandits diff --git a/LeanBandits/ForMathlib/Traj.lean b/LeanBandits/ForMathlib/Traj.lean index d9fdf7e2..8d71107a 100644 --- a/LeanBandits/ForMathlib/Traj.lean +++ b/LeanBandits/ForMathlib/Traj.lean @@ -59,14 +59,16 @@ lemma MeasurableEquiv.coe_prodCongr {α β γ δ : Type*} lemma MeasurableEquiv.coe_refl {α : Type*} {mα : MeasurableSpace α} : (MeasurableEquiv.refl α : α → α) = id := rfl -theorem hasLaw_Iic_of_forall_hasCondDistrib [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] - {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) - (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) - (n : ℕ) : +theorem hasLaw_Iic_of_forall_hasCondDistrib' [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] + {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N n : ℕ} + (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) + (hn : n ≤ N) : HasLaw (fun ω (i : Iic n) ↦ Y i ω) ((partialTraj κ 0 n) ∘ₘ (μ₀.map (MeasurableEquiv.piUnique _).symm)) P := by + revert hn induction n with | zero => + intro _ simp only [piUnique_symm_apply, partialTraj_self, Measure.id_comp] rw [← h0.map_eq, AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)] constructor @@ -84,7 +86,9 @@ theorem hasLaw_Iic_of_forall_hasCondDistrib [∀ n, StandardBorelSpace (X n)] [ rw [Unique.eq_default i] simp [coe_default_Iic_zero] | succ n hn => - specialize h_condDistrib n + intro hn_le + specialize h_condDistrib n (by grind) + specialize hn (by grind) have h_law := hn.prod_of_hasCondDistrib h_condDistrib have : (fun ω (i : Iic (n + 1)) ↦ Y i ω) = (MeasurableEquiv.IicSuccProd X n).symm ∘ @@ -109,6 +113,14 @@ theorem hasLaw_Iic_of_forall_hasCondDistrib [∀ n, StandardBorelSpace (X n)] [ congr simp [MeasurableEquiv.coe_refl] +theorem hasLaw_Iic_of_forall_hasCondDistrib [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] + {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) + (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) + (n : ℕ) : + HasLaw (fun ω (i : Iic n) ↦ Y i ω) + ((partialTraj κ 0 n) ∘ₘ (μ₀.map (MeasurableEquiv.piUnique _).symm)) P := by + exact hasLaw_Iic_of_forall_hasCondDistrib' (N := n) h0 (fun n _ ↦ h_condDistrib n) le_rfl + omit [IsProbabilityMeasure μ₀] in lemma trajMeasure_map_frestrictLe (n : ℕ) : (trajMeasure μ₀ κ).map (frestrictLe n) = @@ -116,6 +128,14 @@ lemma trajMeasure_map_frestrictLe (n : ℕ) : rw [trajMeasure, ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc, Kernel.deterministic_comp_eq_map, traj_map_frestrictLe] +theorem eq_trajMeasure_map_frestrictLe [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] + {Y : (n : ℕ) → Ω → X n} + (h0 : HasLaw (Y 0) μ₀ P) {N : ℕ} + (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) : + P.map (fun ω (n : Iic N) ↦ Y n ω) = (trajMeasure μ₀ κ).map (frestrictLe N) := by + rw [(hasLaw_Iic_of_forall_hasCondDistrib' h0 h_condDistrib le_rfl).map_eq, + trajMeasure_map_frestrictLe] + -- todo: switch to `HasLaw` /-- Uniqueness of `trajMeasure`. -/ theorem eq_trajMeasure [∀ n, StandardBorelSpace (X n)] [∀ n, Nonempty (X n)] diff --git a/LeanBandits/SequentialLearning/Algorithm.lean b/LeanBandits/SequentialLearning/Algorithm.lean index df3c528b..c9e69fc5 100644 --- a/LeanBandits/SequentialLearning/Algorithm.lean +++ b/LeanBandits/SequentialLearning/Algorithm.lean @@ -58,7 +58,7 @@ lemma fst_stepKernel (alg : Algorithm α R) (env : Environment α R) (n : ℕ) : section IsAlgEnvSeq variable {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {alg : Algorithm α R} {env : Environment α R} - {P : Measure Ω} [IsFiniteMeasure P] + {P : Measure Ω} [IsFiniteMeasure P] {N : ℕ} /-- Step of the algorithm-environment sequence: the action-reward pair at time `n`. -/ def IsAlgEnvSeq.step (A : ℕ → Ω → α) (R' : ℕ → Ω → R) (n : ℕ) (ω : Ω) : α × R := @@ -107,18 +107,47 @@ structure IsAlgEnvSeq HasCondDistrib (R' (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A R' n ω, A (n + 1) ω)) (env.feedback n) P +/-- An algorithm-environment sequence: a sequence of actions and rewards generated +by an algorithm interacting with an environment. -/ +structure IsAlgEnvSeqUntil + [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (A : ℕ → Ω → α) (R' : ℕ → Ω → R) (alg : Algorithm α R) (env : Environment α R) + (P : Measure Ω) [IsFiniteMeasure P] (N : ℕ) : Prop where + measurable_A n : Measurable (A n) := by fun_prop + measurable_R n : Measurable (R' n) := by fun_prop + hasLaw_action_zero : HasLaw (fun ω ↦ (A 0 ω)) alg.p0 P + hasCondDistrib_reward_zero : HasCondDistrib (R' 0) (A 0) env.ν0 P + hasCondDistrib_action n (hn : n < N) : + HasCondDistrib (A (n + 1)) (IsAlgEnvSeq.hist A R' n) (alg.policy n) P + hasCondDistrib_reward n (hn : n < N) : + HasCondDistrib (R' (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A R' n ω, A (n + 1) ω)) + (env.feedback n) P + lemma IsAlgEnvSeq.hasLaw_step_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (h : IsAlgEnvSeq A R' alg env P) : HasLaw (step A R' 0) (alg.p0 ⊗ₘ env.ν0) P := HasLaw.prod_of_hasCondDistrib h.hasLaw_action_zero h.hasCondDistrib_reward_zero +lemma IsAlgEnvSeqUntil.hasLaw_step_zero + [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (h : IsAlgEnvSeqUntil A R' alg env P N) : + HasLaw (IsAlgEnvSeq.step A R' 0) (alg.p0 ⊗ₘ env.ν0) P := + HasLaw.prod_of_hasCondDistrib h.hasLaw_action_zero h.hasCondDistrib_reward_zero + lemma IsAlgEnvSeq.hasCondDistrib_step [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (h : IsAlgEnvSeq A R' alg env P) (n : ℕ) : HasCondDistrib (step A R' (n + 1)) (hist A R' n) (stepKernel alg env n) P := HasCondDistrib.prod (h.hasCondDistrib_action n) (h.hasCondDistrib_reward n) +lemma IsAlgEnvSeqUntil.hasCondDistrib_step + [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (h : IsAlgEnvSeqUntil A R' alg env P N) (n : ℕ) (hn : n < N) : + HasCondDistrib (IsAlgEnvSeq.step A R' (n + 1)) (IsAlgEnvSeq.hist A R' n) + (stepKernel alg env n) P := + HasCondDistrib.prod (h.hasCondDistrib_action n hn) (h.hasCondDistrib_reward n hn) + /-- Filtration generated by the history up to time `n`. -/ def IsAlgEnvSeq.filtration (hA : ∀ n, Measurable (A n)) (hR' : ∀ n, Measurable (R' n)) : Filtration ℕ mΩ where @@ -219,7 +248,7 @@ variable {Ω Ω' : Type*} {mΩ : MeasurableSpace Ω} {mΩ' : MeasurableSpace Ω' [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] {alg : Algorithm α R} {env : Environment α R} {P : Measure Ω} [IsProbabilityMeasure P] {P' : Measure Ω'} [IsProbabilityMeasure P'] - {A₁ : ℕ → Ω → α} {R₁ : ℕ → Ω → R} {A₂ : ℕ → Ω' → α} {R₂ : ℕ → Ω' → R} + {A₁ : ℕ → Ω → α} {R₁ : ℕ → Ω → R} {A₂ : ℕ → Ω' → α} {R₂ : ℕ → Ω' → R} {N : ℕ} theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) : P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = trajMeasure alg env := by @@ -234,11 +263,29 @@ theorem eq_trajMeasure_of_isAlgEnvSeq (h : IsAlgEnvSeq A₁ R₁ alg env P) : exact h.hasLaw_step_zero · exact h.hasCondDistrib_step n +lemma eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil + (h : IsAlgEnvSeqUntil A₁ R₁ alg env P N) : + P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) = + (trajMeasure alg env).map (Preorder.frestrictLe N) := by + rw [trajMeasure] + have h := Kernel.eq_trajMeasure_map_frestrictLe (Y := fun n ω ↦ (A₁ n ω, R₁ n ω)) + (P := P) (μ₀ := alg.p0 ⊗ₘ env.ν0) (κ := stepKernel alg env) ?_ (fun n hn ↦ ?_) (N := N) + · exact h + · exact h.hasLaw_step_zero + · exact h.hasCondDistrib_step n hn + theorem isAlgEnvSeq_unique (h1 : IsAlgEnvSeq A₁ R₁ alg env P) (h2 : IsAlgEnvSeq A₂ R₂ alg env P') : P.map (fun ω n ↦ (A₁ n ω, R₁ n ω)) = P'.map (fun ω n ↦ (A₂ n ω, R₂ n ω)) := by rw [eq_trajMeasure_of_isAlgEnvSeq h1, eq_trajMeasure_of_isAlgEnvSeq h2] +theorem isAlgEnvSeqUntil_unique (h1 : IsAlgEnvSeqUntil A₁ R₁ alg env P N) + (h2 : IsAlgEnvSeqUntil A₂ R₂ alg env P' N) : + P.map (fun ω (n : Iic N) ↦ (A₁ n ω, R₁ n ω)) = + P'.map (fun ω (n : Iic N) ↦ (A₂ n ω, R₂ n ω)) := by + rw [eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h1, + eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil h2] + end ModelEquivalence end Learning From 6a716170cb290d0a568df0a401303f8f52668a24 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 22 Jan 2026 15:06:51 +0100 Subject: [PATCH 2/5] use IsAlgEnvSeqUntil --- LeanBandits/BanditAlgorithms/RoundRobin.lean | 24 +++++++------- LeanBandits/SequentialLearning/Algorithm.lean | 21 ++++++++++++ .../SequentialLearning/Deterministic.lean | 32 +++++++++++++++++++ 3 files changed, 65 insertions(+), 12 deletions(-) diff --git a/LeanBandits/BanditAlgorithms/RoundRobin.lean b/LeanBandits/BanditAlgorithms/RoundRobin.lean index e8021c60..fb46cd06 100644 --- a/LeanBandits/BanditAlgorithms/RoundRobin.lean +++ b/LeanBandits/BanditAlgorithms/RoundRobin.lean @@ -50,34 +50,34 @@ variable {hK : 0 < K} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν] {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} lemma arm_zero [Nonempty (Fin K)] - (h : IsAlgEnvSeq A R (roundRobinAlgorithm hK) (stationaryEnv ν) P) : + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P 0) : A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ := by have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK exact h.action_zero_detAlgorithm -lemma arm_ae_eq_roundRobinNextArm [Nonempty (Fin K)] - (h : IsAlgEnvSeq A R (roundRobinAlgorithm hK) (stationaryEnv ν) P) (n : ℕ) : - A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK n (IsAlgEnvSeq.hist A R n ω) := by - have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK - exact h.action_detAlgorithm_ae_eq n +lemma arm_ae_eq_roundRobinNextArm [Nonempty (Fin K)] (n : ℕ) + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (n + 1)) : + A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK n (IsAlgEnvSeq.hist A R n ω) := + h.action_detAlgorithm_ae_eq (by grind) /-- The arm pulled at time `n` is the arm `n % K`. -/ -lemma arm_ae_eq [Nonempty (Fin K)] - (h : IsAlgEnvSeq A R (roundRobinAlgorithm hK) (stationaryEnv ν) P) (n : ℕ) : +lemma arm_ae_eq [Nonempty (Fin K)] (n : ℕ) + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P n) : A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := by cases n with | zero => exact arm_zero h | succ n => - filter_upwards [arm_ae_eq_roundRobinNextArm h n] with h hn_eq + filter_upwards [arm_ae_eq_roundRobinNextArm n h] with h hn_eq rw [hn_eq, nextArm] /-- At time `K * m`, the number of pulls of each arm is equal to `m`. -/ -lemma pullCount_mul [Nonempty (Fin K)] - (h : IsAlgEnvSeq A R (roundRobinAlgorithm hK) (stationaryEnv ν) P) (a : Fin K) (m : ℕ) : +lemma pullCount_mul [Nonempty (Fin K)] (m : ℕ) + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K * m)) (a : Fin K) : pullCount A a (K * m) =ᵐ[P] fun _ ↦ m := by rw [Filter.EventuallyEq] simp_rw [pullCount_eq_sum] - have h_arm (n : range (K * m)) : A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := arm_ae_eq h n + have h_arm (n : range (K * m)) : A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := + arm_ae_eq n (h.mono (by have := n.2; simp only [mem_range] at this; grind)) simp_rw [Filter.EventuallyEq, ← ae_all_iff] at h_arm filter_upwards [h_arm] with ω h_arm have h_arm' {i : ℕ} (hi : i ∈ range (K * m)) : A i ω = ⟨i % K, Nat.mod_lt _ hK⟩ := h_arm ⟨i, hi⟩ diff --git a/LeanBandits/SequentialLearning/Algorithm.lean b/LeanBandits/SequentialLearning/Algorithm.lean index c9e69fc5..d79c5c8e 100644 --- a/LeanBandits/SequentialLearning/Algorithm.lean +++ b/LeanBandits/SequentialLearning/Algorithm.lean @@ -123,6 +123,27 @@ structure IsAlgEnvSeqUntil HasCondDistrib (R' (n + 1)) (fun ω ↦ (IsAlgEnvSeq.hist A R' n ω, A (n + 1) ω)) (env.feedback n) P +lemma IsAlgEnvSeqUntil.mono [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (h : IsAlgEnvSeqUntil A R' alg env P N) {N' : ℕ} (hN : N' ≤ N) : + IsAlgEnvSeqUntil A R' alg env P N' where + measurable_A := h.measurable_A + measurable_R := h.measurable_R + hasLaw_action_zero := h.hasLaw_action_zero + hasCondDistrib_reward_zero := h.hasCondDistrib_reward_zero + hasCondDistrib_action n hn := h.hasCondDistrib_action n (hn.trans_le hN) + hasCondDistrib_reward n hn := h.hasCondDistrib_reward n (hn.trans_le hN) + +lemma IsAlgEnvSeq.isAlgEnvSeqUntil + [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + (h : IsAlgEnvSeq A R' alg env P) (N : ℕ) : + IsAlgEnvSeqUntil A R' alg env P N where + measurable_A := h.measurable_A + measurable_R := h.measurable_R + hasLaw_action_zero := h.hasLaw_action_zero + hasCondDistrib_reward_zero := h.hasCondDistrib_reward_zero + hasCondDistrib_action n _ := h.hasCondDistrib_action n + hasCondDistrib_reward n _ := h.hasCondDistrib_reward n + lemma IsAlgEnvSeq.hasLaw_step_zero [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] (h : IsAlgEnvSeq A R' alg env P) : diff --git a/LeanBandits/SequentialLearning/Deterministic.lean b/LeanBandits/SequentialLearning/Deterministic.lean index 5ab42a05..91ef55e2 100644 --- a/LeanBandits/SequentialLearning/Deterministic.lean +++ b/LeanBandits/SequentialLearning/Deterministic.lean @@ -67,6 +67,38 @@ lemma action_detAlgorithm_ae_all_eq end IsAlgEnvSeq +namespace IsAlgEnvSeqUntil + +variable {Ω : Type*} {mΩ : MeasurableSpace Ω} + [StandardBorelSpace α] [Nonempty α] [StandardBorelSpace R] [Nonempty R] + {alg : Algorithm α R} {ν : Kernel α R} [IsMarkovKernel ν] + {P : Measure Ω} [IsProbabilityMeasure P] {A : ℕ → Ω → α} {R' : ℕ → Ω → R} {N n : ℕ} + +lemma HasLaw_action_zero_detAlgorithm + (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextAction h_next action0) env P N) : + HasLaw (A 0) (Measure.dirac action0) P where + aemeasurable := have hA := h.measurable_A; by fun_prop + map_eq := (hasLaw_action_zero h).map_eq + +lemma action_zero_detAlgorithm + (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextAction h_next action0) env P N) : + A 0 =ᵐ[P] fun _ ↦ action0 := by + have h_eq : ∀ᵐ x ∂(P.map (A 0)), x = action0 := by + rw [(hasLaw_action_zero h).map_eq] + simp [detAlgorithm] + have hA := h.measurable_A + exact ae_of_ae_map (by fun_prop) h_eq + +lemma action_detAlgorithm_ae_eq + (h : IsAlgEnvSeqUntil A R' (detAlgorithm nextAction h_next action0) env P N) (hn : n < N) : + A (n + 1) =ᵐ[P] fun ω ↦ nextAction n (IsAlgEnvSeq.hist A R' n ω) := by + have hA := h.measurable_A + have hR' := h.measurable_R + exact ae_eq_of_condDistrib_eq_deterministic (by fun_prop) (by fun_prop) (by fun_prop) + (h.hasCondDistrib_action n hn).condDistrib_eq + +end IsAlgEnvSeqUntil + namespace IT local notation "𝔓" => trajMeasure (detAlgorithm nextAction h_next action0) env From 8da4973ed21663fbe53e8325b61f386447f682cd Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 22 Jan 2026 15:10:00 +0100 Subject: [PATCH 3/5] lint --- LeanBandits/BanditAlgorithms/RoundRobin.lean | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/LeanBandits/BanditAlgorithms/RoundRobin.lean b/LeanBandits/BanditAlgorithms/RoundRobin.lean index fb46cd06..0c315ab7 100644 --- a/LeanBandits/BanditAlgorithms/RoundRobin.lean +++ b/LeanBandits/BanditAlgorithms/RoundRobin.lean @@ -25,20 +25,13 @@ section AlgorithmDefinition /-- Arm pulled by the Round-Robin algorithm at time `n + 1`. This is arm `n % K`. -/ noncomputable -def RoundRobin.nextArm (hK : 0 < K) (n : ℕ) (_h : Iic n → Fin K × ℝ) : Fin K := - ⟨(n + 1) % K, Nat.mod_lt _ hK⟩ -- for `n = 0` we have pulled arm 0 already, and we pull arm 1 - -/-- The next arm pulled by Round-Robin is chosen in a measurable way. -/ -@[fun_prop] -lemma RoundRobin.measurable_nextArm (hK : 0 < K) (n : ℕ) : Measurable (nextArm hK n) := by - unfold nextArm - fun_prop +def RoundRobin.nextArm (hK : 0 < K) (n : ℕ) : Fin K := ⟨(n + 1) % K, Nat.mod_lt _ hK⟩ /-- The Round-Robin algorithm: deterministic algorithm that chooses the next arm according to `RoundRobin.nextArm`. -/ noncomputable def roundRobinAlgorithm (hK : 0 < K) : Algorithm (Fin K) ℝ := - detAlgorithm (RoundRobin.nextArm hK) (by fun_prop) ⟨0, hK⟩ + detAlgorithm (fun n _ ↦ RoundRobin.nextArm hK n) (by fun_prop) ⟨0, hK⟩ end AlgorithmDefinition @@ -57,7 +50,7 @@ lemma arm_zero [Nonempty (Fin K)] lemma arm_ae_eq_roundRobinNextArm [Nonempty (Fin K)] (n : ℕ) (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (n + 1)) : - A (n + 1) =ᵐ[P] fun ω ↦ nextArm hK n (IsAlgEnvSeq.hist A R n ω) := + A (n + 1) =ᵐ[P] fun _ ↦ nextArm hK n := h.action_detAlgorithm_ae_eq (by grind) /-- The arm pulled at time `n` is the arm `n % K`. -/ From e946e0f74cfd730ce3ce6a1d3787ed4e5d55d8f2 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 22 Jan 2026 15:47:28 +0100 Subject: [PATCH 4/5] refactor etc and ucb --- LeanBandits/BanditAlgorithms/ETC.lean | 47 +++++++++-------- LeanBandits/BanditAlgorithms/RoundRobin.lean | 39 ++++++++++++-- LeanBandits/BanditAlgorithms/UCB.lean | 54 ++++++++++---------- 3 files changed, 86 insertions(+), 54 deletions(-) diff --git a/LeanBandits/BanditAlgorithms/ETC.lean b/LeanBandits/BanditAlgorithms/ETC.lean index b49c4f3a..e1e55c7c 100644 --- a/LeanBandits/BanditAlgorithms/ETC.lean +++ b/LeanBandits/BanditAlgorithms/ETC.lean @@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne -/ import LeanBandits.Bandit.SumRewards -import LeanBandits.BanditAlgorithms.AuxSums +import LeanBandits.BanditAlgorithms.RoundRobin import LeanBandits.ForMathlib.MeasurableArgMax -import LeanBandits.SequentialLearning.Deterministic /-! # The Explore-Then-Commit Algorithm @@ -70,11 +69,26 @@ variable {hK : 0 < K} {m : ℕ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν] {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {σ2 : ℝ≥0} +/-- Until round `K * m - 1`, the ETC algorithm behaves like the Round-Robin algorithm. -/ +lemma isAlgEnvSeqUntil_roundRobinAlgorithm [Nonempty (Fin K)] + (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) : + IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K * m - 1) where + measurable_A := h.measurable_A + measurable_R := h.measurable_R + hasLaw_action_zero := h.hasLaw_action_zero + hasCondDistrib_reward_zero := h.hasCondDistrib_reward_zero + hasCondDistrib_action n hn := by + convert h.hasCondDistrib_action n using 1 + simp only [roundRobinAlgorithm, detAlgorithm_policy, etcAlgorithm] + congr 1 with h + unfold ETC.nextArm RoundRobin.nextArm + simp [hn] + hasCondDistrib_reward n _ := h.hasCondDistrib_reward n + lemma arm_zero [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) : - A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ := by - have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK - exact h.action_zero_detAlgorithm + A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ := + RoundRobin.arm_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono zero_le') lemma arm_ae_eq_etcNextArm [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (n : ℕ) : @@ -85,13 +99,8 @@ lemma arm_ae_eq_etcNextArm [Nonempty (Fin K)] /-- For `n < K * m`, the arm pulled at time `n` is the arm `n % K`. -/ lemma arm_of_lt [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) {n : ℕ} (hn : n < K * m) : - A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := by - cases n with - | zero => exact arm_zero h - | succ n => - filter_upwards [arm_ae_eq_etcNextArm h n] with h hn_eq - rw [hn_eq, nextArm, dif_pos] - grind + A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := + RoundRobin.arm_ae_eq n ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono (by grind)) /-- The arm pulled at time `K * m` is the arm with the highest empirical mean after the exploration phase. -/ @@ -133,18 +142,8 @@ lemma arm_of_ge [Nonempty (Fin K)] /-- At time `K * m`, the number of pulls of each arm is equal to `m`. -/ lemma pullCount_mul [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) (a : Fin K) : - pullCount A a (K * m) =ᵐ[P] fun _ ↦ m := by - rw [Filter.EventuallyEq] - simp_rw [pullCount_eq_sum] - have h_arm (n : range (K * m)) : A n =ᵐ[P] fun _ ↦ ⟨n % K, Nat.mod_lt _ hK⟩ := - arm_of_lt h (mem_range.mp n.2) - simp_rw [Filter.EventuallyEq, ← ae_all_iff] at h_arm - filter_upwards [h_arm] with ω h_arm - have h_arm' {i : ℕ} (hi : i ∈ range (K * m)) : A i ω = ⟨i % K, Nat.mod_lt _ hK⟩ := h_arm ⟨i, hi⟩ - calc (∑ s ∈ range (K * m), if A s ω = a then 1 else 0) - _ = (∑ s ∈ range (K * m), if ⟨s % K, Nat.mod_lt _ hK⟩ = a then 1 else 0) := - sum_congr rfl fun s hs ↦ by rw [h_arm' hs] - _ = m := sum_mod_range_mul hK m a + pullCount A a (K * m) =ᵐ[P] fun _ ↦ m := + RoundRobin.pullCount_mul m (isAlgEnvSeqUntil_roundRobinAlgorithm h) a lemma pullCount_add_one_of_ge [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (etcAlgorithm hK m) (stationaryEnv ν) P) diff --git a/LeanBandits/BanditAlgorithms/RoundRobin.lean b/LeanBandits/BanditAlgorithms/RoundRobin.lean index 0c315ab7..07d5961c 100644 --- a/LeanBandits/BanditAlgorithms/RoundRobin.lean +++ b/LeanBandits/BanditAlgorithms/RoundRobin.lean @@ -3,10 +3,10 @@ Copyright (c) 2025 Rémy Degenne. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne -/ -import LeanBandits.Bandit.SumRewards import LeanBandits.BanditAlgorithms.AuxSums -import LeanBandits.ForMathlib.MeasurableArgMax import LeanBandits.SequentialLearning.Deterministic +import LeanBandits.SequentialLearning.FiniteActions +import LeanBandits.SequentialLearning.StationaryEnv /-! # Round-Robin algorithm @@ -65,7 +65,8 @@ lemma arm_ae_eq [Nonempty (Fin K)] (n : ℕ) /-- At time `K * m`, the number of pulls of each arm is equal to `m`. -/ lemma pullCount_mul [Nonempty (Fin K)] (m : ℕ) - (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K * m)) (a : Fin K) : + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K * m - 1)) + (a : Fin K) : pullCount A a (K * m) =ᵐ[P] fun _ ↦ m := by rw [Filter.EventuallyEq] simp_rw [pullCount_eq_sum] @@ -79,6 +80,38 @@ lemma pullCount_mul [Nonempty (Fin K)] (m : ℕ) sum_congr rfl fun s hs ↦ by rw [h_arm' hs] _ = m := sum_mod_range_mul hK m a +lemma pullCount_eq_one [Nonempty (Fin K)] + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) + (a : Fin K) : + pullCount A a K =ᵐ[P] fun _ ↦ 1 := by + suffices pullCount A a (K * 1) =ᵐ[P] fun _ ↦ 1 by simpa using this + refine pullCount_mul 1 (P := P) (ν := ν) (R := R) (hK := hK) ?_ a + simpa + +lemma time_gt_of_pullCount_gt_one [Nonempty (Fin K)] + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) (a : Fin K) : + ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n := by + filter_upwards [pullCount_eq_one h a] with h h_eq n hn + rw [← h_eq] at hn + by_contra! h_lt + exact hn.not_ge (pullCount_mono _ h_lt _) + +lemma pullCount_pos_of_time_ge [Nonempty (Fin K)] + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) : + ∀ᵐ ω ∂P, ∀ n, K ≤ n → ∀ b : Fin K, 0 < pullCount A b n ω := by + have h_ae a := pullCount_eq_one h a + simp_rw [Filter.EventuallyEq, ← ae_all_iff] at h_ae + filter_upwards [h_ae] with ω hω n hn a + refine Nat.one_pos.trans_le ?_ + rw [← hω a] + exact pullCount_mono _ hn _ + +lemma pullCount_pos_of_pullCount_gt_one [Nonempty (Fin K)] + (h : IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1)) (a : Fin K) : + ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω := by + filter_upwards [time_gt_of_pullCount_gt_one h a, pullCount_pos_of_time_ge h] with ω h1 h2 n h_gt a + exact h2 n (h1 n h_gt).le a + end RoundRobin end Bandits diff --git a/LeanBandits/BanditAlgorithms/UCB.lean b/LeanBandits/BanditAlgorithms/UCB.lean index 1aa5d1de..c73d4645 100644 --- a/LeanBandits/BanditAlgorithms/UCB.lean +++ b/LeanBandits/BanditAlgorithms/UCB.lean @@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémy Degenne -/ import LeanBandits.Bandit.SumRewards -import LeanBandits.BanditAlgorithms.AuxSums +import LeanBandits.BanditAlgorithms.RoundRobin import LeanBandits.ForMathlib.MeasurableArgMax -import LeanBandits.SequentialLearning.Deterministic /-! # UCB algorithm @@ -59,6 +58,22 @@ variable {hK : 0 < K} {c : ℝ} {ν : Kernel (Fin K) ℝ} [IsMarkovKernel ν] {A : ℕ → Ω → Fin K} {R : ℕ → Ω → ℝ} {σ2 : ℝ≥0} {n : ℕ} {ω : Ω} +/-- Until round `K - 1`, the UCB algorithm behaves like the Round-Robin algorithm. -/ +lemma isAlgEnvSeqUntil_roundRobinAlgorithm [Nonempty (Fin K)] + (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) : + IsAlgEnvSeqUntil A R (roundRobinAlgorithm hK) (stationaryEnv ν) P (K - 1) where + measurable_A := h.measurable_A + measurable_R := h.measurable_R + hasLaw_action_zero := h.hasLaw_action_zero + hasCondDistrib_reward_zero := h.hasCondDistrib_reward_zero + hasCondDistrib_action n hn := by + convert h.hasCondDistrib_action n using 1 + simp only [roundRobinAlgorithm, detAlgorithm_policy, ucbAlgorithm] + congr 1 with h + unfold UCB.nextArm RoundRobin.nextArm + simp [hn] + hasCondDistrib_reward n _ := h.hasCondDistrib_reward n + /-- The exploration bonus of the UCB algorithm, which corresponds to the width of a confidence interval. -/ noncomputable def ucbWidth (A : ℕ → Ω → Fin K) (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) : ℝ := @@ -80,9 +95,8 @@ lemma ucbWidth_eq_ucbWidth' (c : ℝ) (a : Fin K) (n : ℕ) (ω : Ω) (hn : n lemma arm_zero [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) : - A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ := by - have : Nonempty (Fin K) := Fin.pos_iff_nonempty.mp hK - exact h.action_zero_detAlgorithm + A 0 =ᵐ[P] fun _ ↦ ⟨0, hK⟩ := + RoundRobin.arm_zero ((isAlgEnvSeqUntil_roundRobinAlgorithm h).mono zero_le') lemma arm_ae_eq_ucbNextArm [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (n : ℕ) : @@ -147,37 +161,23 @@ lemma forall_arm_prop [Nonempty (Fin K)] lemma pullCount_eq_of_time_eq [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) : - ∀ᵐ ω ∂P, pullCount A a K ω = 1 := by - filter_upwards [forall_arm_eq_mod_of_lt h] with h h_eq - rw [pullCount_eq_sum] - conv_rhs => rw [← sum_mod_range hK a] - refine Finset.sum_congr rfl fun s hs ↦ ?_ - congr - exact h_eq s (by grind) + ∀ᵐ ω ∂P, pullCount A a K ω = 1 := + RoundRobin.pullCount_eq_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a lemma time_gt_of_pullCount_gt_one [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) : - ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n := by - filter_upwards [pullCount_eq_of_time_eq h a] with h h_eq n hn - rw [← h_eq] at hn - by_contra! h_lt - exact hn.not_ge (pullCount_mono _ h_lt _) + ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n := + RoundRobin.time_gt_of_pullCount_gt_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a lemma pullCount_pos_of_time_ge [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) : - ∀ᵐ ω ∂P, ∀ n, K ≤ n → ∀ b : Fin K, 0 < pullCount A b n ω := by - have h_ae a := pullCount_eq_of_time_eq h a - rw [← ae_all_iff] at h_ae - filter_upwards [h_ae] with ω hω n hn a - refine Nat.one_pos.trans_le ?_ - rw [← hω a] - exact pullCount_mono _ hn _ + ∀ᵐ ω ∂P, ∀ n, K ≤ n → ∀ b : Fin K, 0 < pullCount A b n ω := + RoundRobin.pullCount_pos_of_time_ge (isAlgEnvSeqUntil_roundRobinAlgorithm h) lemma pullCount_pos_of_pullCount_gt_one [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) : - ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω := by - filter_upwards [time_gt_of_pullCount_gt_one h a, pullCount_pos_of_time_ge h] with ω h1 h2 n h_gt a - exact h2 n (h1 n h_gt).le a + ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω := + RoundRobin.pullCount_pos_of_pullCount_gt_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a omit [IsMarkovKernel ν] in lemma gap_arm_le_two_mul_ucbWidth [Nonempty (Fin K)] From d31f74fdb37fe9bf48e442df05467a63e9c5e751 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 22 Jan 2026 21:52:45 +0100 Subject: [PATCH 5/5] add blueprint section for Round-Robin --- LeanBandits/BanditAlgorithms/UCB.lean | 10 ------ blueprint/lean_decls | 5 +++ blueprint/src/chapters/etc.tex | 52 ++++++++++++++++++++++++++- blueprint/src/chapters/ucb.tex | 14 ++++++++ 4 files changed, 70 insertions(+), 11 deletions(-) diff --git a/LeanBandits/BanditAlgorithms/UCB.lean b/LeanBandits/BanditAlgorithms/UCB.lean index 9906d71e..806a2a12 100644 --- a/LeanBandits/BanditAlgorithms/UCB.lean +++ b/LeanBandits/BanditAlgorithms/UCB.lean @@ -161,21 +161,11 @@ lemma forall_arm_prop [Nonempty (Fin K)] simp_rw [ae_all_iff] at h_ae exact h_ae n hn -lemma pullCount_eq_of_time_eq [Nonempty (Fin K)] - (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) : - ∀ᵐ ω ∂P, pullCount A a K ω = 1 := - RoundRobin.pullCount_eq_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a - lemma time_gt_of_pullCount_gt_one [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) : ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → K < n := RoundRobin.time_gt_of_pullCount_gt_one (isAlgEnvSeqUntil_roundRobinAlgorithm h) a -lemma pullCount_pos_of_time_ge [Nonempty (Fin K)] - (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) : - ∀ᵐ ω ∂P, ∀ n, K ≤ n → ∀ b : Fin K, 0 < pullCount A b n ω := - RoundRobin.pullCount_pos_of_time_ge (isAlgEnvSeqUntil_roundRobinAlgorithm h) - lemma pullCount_pos_of_pullCount_gt_one [Nonempty (Fin K)] (h : IsAlgEnvSeq A R (ucbAlgorithm hK c) (stationaryEnv ν) P) (a : Fin K) : ∀ᵐ ω ∂P, ∀ n, 1 < pullCount A a n ω → ∀ b : Fin K, 0 < pullCount A b n ω := diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 003554c0..274ca679 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -108,14 +108,19 @@ Bandits.probReal_sumRewards_le_sumRewards_le Bandits.probReal_sum_le_sum_streamMeasure Bandits.prob_sum_le_sqrt_log Bandits.prob_sum_ge_sqrt_log +Bandits.RoundRobin.nextArm +Bandits.roundRobinAlgorithm +Bandits.RoundRobin.pullCount_mul Bandits.ETC.nextArm Bandits.etcAlgorithm +Bandits.ETC.isAlgEnvSeqUntil_roundRobinAlgorithm Bandits.ETC.pullCount_of_ge Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq Bandits.ETC.prob_arm_mul_eq_le Bandits.ETC.regret_le Bandits.UCB.nextArm Bandits.ucbAlgorithm +Bandits.UCB.isAlgEnvSeqUntil_roundRobinAlgorithm Bandits.UCB.ucbIndex_le_ucbIndex_arm Bandits.UCB.gap_arm_le_two_mul_ucbWidth Bandits.UCB.pullCount_arm_le diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex index 7bec9e10..2fda856e 100644 --- a/blueprint/src/chapters/etc.tex +++ b/blueprint/src/chapters/etc.tex @@ -1,5 +1,41 @@ \chapter{Bandit algorithms} +\section{Round-Robin} + +This is not an interesting bandit algorithm per se, but it is used as a subroutine in other algorithms and can be a simple baseline. +This algorithm simply cycles through the arms in order. + +\begin{definition}\label{def:roundRobinAlgorithm} + \uses{def:detAlgorithm,def:algorithm} + \leanok + \lean{Bandits.RoundRobin.nextArm, Bandits.roundRobinAlgorithm} +The Round-Robin algorithm is defined as follows: at time $t \in \mathbb{N}$, $A_t = t \mod K$. +\end{definition} + + +\begin{lemma}\label{lem:pullCount_roundRobinAlgorithm} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:pullCount,def:roundRobinAlgorithm} + \leanok + \lean{Bandits.RoundRobin.pullCount_mul} +For the Round-Robin algorithm, for any arm $a \in [K]$, at time $Km$ we have +\begin{align*} + N_{Km,a} + &= m + \: . +\end{align*} +\end{lemma} + +\begin{proof}\leanok + \uses{def:environment,def:detAlgorithm,def:algorithm,def:history,lem:pullCount_basic,def:roundRobinAlgorithm} + +\end{proof} + + +TODO: regret. + + + + \section{Explore-Then-Commit} Note: times start at 0 to be consistent with Lean. @@ -19,6 +55,20 @@ \section{Explore-Then-Commit} \end{definition} +\begin{lemma}\label{lem:ETC.isAlgEnvSeqUntil_roundRobinAlgorithm} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:etcAlgorithm,def:roundRobinAlgorithm} + \leanok + \lean{Bandits.ETC.isAlgEnvSeqUntil_roundRobinAlgorithm} +An algorithm-environment sequence for the Explore-Then-Commit algorithm with parameter $m$ is an algorithm-environment sequence for the Round-Robin algorithm until time $Km - 1$. +That is, ETC plays the same as Round-Robin until time $Km - 1$. +\end{lemma} + +\begin{proof} + \leanok + +\end{proof} + + \begin{lemma}\label{lem:pullCount_etcAlgorithm} \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:pullCount,def:etcAlgorithm} \leanok @@ -32,7 +82,7 @@ \section{Explore-Then-Commit} \end{lemma} \begin{proof}\leanok - \uses{def:environment,def:detAlgorithm,def:algorithm,def:history,lem:pullCount_basic,def:etcAlgorithm} + \uses{def:environment,def:detAlgorithm,def:algorithm,def:history,lem:pullCount_basic,def:etcAlgorithm,lem:pullCount_roundRobinAlgorithm,lem:ETC.isAlgEnvSeqUntil_roundRobinAlgorithm} \end{proof} diff --git a/blueprint/src/chapters/ucb.tex b/blueprint/src/chapters/ucb.tex index 653b98a9..1290d450 100644 --- a/blueprint/src/chapters/ucb.tex +++ b/blueprint/src/chapters/ucb.tex @@ -14,6 +14,20 @@ \section{UCB} Note: the argmax in the second step is chosen in a measurable way. +\begin{lemma}\label{lem:UCB.isAlgEnvSeqUntil_roundRobinAlgorithm} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm,def:roundRobinAlgorithm} + \leanok + \lean{Bandits.UCB.isAlgEnvSeqUntil_roundRobinAlgorithm} +An algorithm-environment sequence for the UCB algorithm is an algorithm-environment sequence for the Round-Robin algorithm until time $K - 1$. +That is, UCB plays the same as Round-Robin until time $K - 1$. +\end{lemma} + +\begin{proof} + \leanok + +\end{proof} + + \begin{lemma}\label{lem:ucbIndex_le_ucbIndex_arm} \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm,def:pullCount,def:empMean} \leanok