From 6fb61106443b61f945defb39dfdbdb7042a08b81 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 18 Jan 2026 21:42:08 +0100 Subject: [PATCH] delete unnecessary defs --- LeanBandits/Bandit/Bandit.lean | 90 ++++------------ LeanBandits/Bandit/RewardByCountMeasure.lean | 102 +------------------ LeanBandits/Bandit/SumRewards.lean | 52 +++++----- LeanBandits/BanditAlgorithms/ETC.lean | 1 + LeanBandits/BanditAlgorithms/UCB.lean | 29 +++--- blueprint/lean_decls | 2 - blueprint/src/chapters/bandit.tex | 11 -- 7 files changed, 65 insertions(+), 222 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index a53c2b60..27f62a02 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -8,7 +8,6 @@ import LeanBandits.ForMathlib.IndepFun import LeanBandits.ForMathlib.IndepInfinitePi import LeanBandits.ForMathlib.KernelRepresentation import LeanBandits.ForMathlib.StandardBorel -import LeanBandits.SequentialLearning.Deterministic import LeanBandits.SequentialLearning.FiniteActions import LeanBandits.SequentialLearning.StationaryEnv @@ -26,32 +25,6 @@ variable {α R : Type*} {mα : MeasurableSpace α} {mR : MeasurableSpace R} section MeasureSpace -namespace Bandit - -/-- Kernel describing the distribution of the next action-reward pair given the history up to -time `n`. -/ -noncomputable -def stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : - Kernel (Iic n → α × R) (α × R) := - Learning.stepKernel alg (stationaryEnv ν) n -deriving IsMarkovKernel - -@[simp] -lemma fst_stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : - (stepKernel alg ν n).fst = alg.policy n := by - rw [stepKernel, Learning.fst_stepKernel] - -@[simp] -lemma snd_stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : - (stepKernel alg ν n).snd = ν ∘ₖ alg.policy n := by - rw [stepKernel, Learning.stepKernel, stationaryEnv_feedback, Kernel.snd_compProd_prodMkLeft] - -/-- Measure on the sequence of actions pulled and rewards observed generated by the bandit. -/ -noncomputable -def trajMeasure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : Measure (ℕ → α × R) := - Learning.trajMeasure alg (stationaryEnv ν) -deriving IsProbabilityMeasure - /-- Measure of an infinite stream of rewards from each action. -/ noncomputable def streamMeasure (ν : Kernel α R) : Measure (ℕ → α → R) := @@ -61,26 +34,6 @@ instance (ν : Kernel α R) [IsMarkovKernel ν] : IsProbabilityMeasure (streamMe unfold streamMeasure infer_instance -/-- Joint distribution of the sequence of action pulled and rewards, and a stream of independent -rewards from all actions. -/ -noncomputable -def measure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : - Measure ((ℕ → α × R) × (ℕ → α → R)) := - (trajMeasure alg ν).prod (streamMeasure ν) -deriving IsProbabilityMeasure - -@[simp] -lemma fst_measure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : - (measure alg ν).fst = trajMeasure alg ν := by - rw [measure, Measure.fst_prod] - -@[simp] -lemma snd_measure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : - (measure alg ν).snd = streamMeasure ν := by - rw [measure, Measure.snd_prod] - -end Bandit - section StreamMeasure lemma _root_.hasLaw_eval_infinitePi {ι : Type*} {X : ι → Type*} {mX : ∀ i, MeasurableSpace (X i)} @@ -90,15 +43,15 @@ lemma _root_.hasLaw_eval_infinitePi {ι : Type*} {X : ι → Type*} {mX : ∀ i, map_eq := by exact (measurePreserving_eval_infinitePi μ i).map_eq lemma hasLaw_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : - HasLaw (fun h : ℕ → α → R ↦ h n) (Measure.infinitePi ν) (Bandit.streamMeasure ν) := + HasLaw (fun h : ℕ → α → R ↦ h n) (Measure.infinitePi ν) (streamMeasure ν) := hasLaw_eval_infinitePi (fun _ ↦ Measure.infinitePi ν) n lemma hasLaw_eval_eval_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) (a : α) : - HasLaw (fun h : ℕ → α → R ↦ h n a) (ν a) (Bandit.streamMeasure ν) := + HasLaw (fun h : ℕ → α → R ↦ h n a) (ν a) (streamMeasure ν) := (hasLaw_eval_infinitePi ν a).comp (hasLaw_eval_streamMeasure ν n) lemma identDistrib_eval_eval_id_streamMeasure (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) (a : α) : - IdentDistrib (fun h : ℕ → α → R ↦ h n a) id (Bandit.streamMeasure ν) (ν a) where + IdentDistrib (fun h : ℕ → α → R ↦ h n a) id (streamMeasure ν) (ν a) where aemeasurable_fst := Measurable.aemeasurable (by fun_prop) aemeasurable_snd := Measurable.aemeasurable (by fun_prop) map_eq := by @@ -118,47 +71,40 @@ lemma Integrable.congr_identDistrib {Ω Ω' : Type*} lemma integrable_eval_streamMeasure (ν : Kernel α ℝ) [IsMarkovKernel ν] (n : ℕ) (a : α) (h_int : Integrable id (ν a)) : - Integrable (fun h : ℕ → α → ℝ ↦ h n a) (Bandit.streamMeasure ν) := + Integrable (fun h : ℕ → α → ℝ ↦ h n a) (streamMeasure ν) := Integrable.congr_identDistrib h_int (identDistrib_eval_eval_id_streamMeasure ν n a).symm lemma integral_eval_streamMeasure (ν : Kernel α ℝ) [IsMarkovKernel ν] (n : ℕ) (a : α) : - ∫ h, h n a ∂(Bandit.streamMeasure ν) = (ν a)[id] := by - calc ∫ h, h n a ∂(Bandit.streamMeasure ν) - _ = ∫ x, x ∂((Bandit.streamMeasure ν).map (fun h ↦ h n a)) := by + ∫ h, h n a ∂(streamMeasure ν) = (ν a)[id] := by + calc ∫ h, h n a ∂(streamMeasure ν) + _ = ∫ x, x ∂((streamMeasure ν).map (fun h ↦ h n a)) := by 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 n ω ↦ ω n) (Bandit.streamMeasure ν) := + iIndepFun (fun n ω ↦ ω n) (streamMeasure ν) := 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 (fun n ω ↦ ω n a) (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 ν) := + iIndepFun (fun (p : ℕ × α) ω ↦ ω p.1 p.2) (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) : - IndepFun (fun ω ↦ ω n a) (fun ω ↦ ω m b) (Bandit.streamMeasure ν) := by + IndepFun (fun ω ↦ ω n a) (fun ω ↦ ω m b) (streamMeasure ν) := by change IndepFun (fun ω ↦ ω (n, a).1 (n, a).2) (fun ω ↦ ω (m, b).1 (m, b).2) - (Bandit.streamMeasure ν) + (streamMeasure ν) exact (iIndepFun_eval_streamMeasure ν).indepFun (by grind) lemma indepFun_eval_streamMeasure' (ν : Kernel α R) [IsMarkovKernel ν] {a b : α} (h : a ≠ b) : - IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (Bandit.streamMeasure ν) := + IndepFun (fun ω n ↦ ω n a) (fun ω n ↦ ω n b) (streamMeasure ν) := indepFun_proj_infinitePi_infinitePi h -lemma indepFun_eval_snd_measure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] - {a b : α} (h : a ≠ b) : - IndepFun (fun ω n ↦ ω.2 n a) (fun ω n ↦ ω.2 n b) (Bandit.measure alg ν) := by - refine indepFun_snd_prod ?_ ?_ (indepFun_eval_streamMeasure' ν h) (Bandit.trajMeasure alg ν) - · exact Measurable.aemeasurable (by fun_prop) - · exact Measurable.aemeasurable (by fun_prop) - end StreamMeasure namespace ArrayModel @@ -181,7 +127,7 @@ instance {α R : Type*} [Countable α] [MeasurableSpace R] [StandardBorelSpace R /-- Probability measure for the array model of stochastic bandits. -/ noncomputable def arrayMeasure (ν : Kernel α R) : Measure (probSpace α R) := - (Measure.infinitePi fun _ ↦ volume).prod (Bandit.streamMeasure ν) + (Measure.infinitePi fun _ ↦ volume).prod (streamMeasure ν) instance (ν : Kernel α R) [IsMarkovKernel ν] : IsProbabilityMeasure (arrayMeasure ν) := Measure.prod.instIsProbabilityMeasure _ _ @@ -606,7 +552,7 @@ lemma map_snd_apply_arrayMeasure {ν : Kernel α R} [IsMarkovKernel ν] (n : ℕ rw [Measure.snd, Measure.map_map (by fun_prop) (by fun_prop)] rfl _ = ν a := by - rw [arrayMeasure, Measure.snd_prod, Bandit.streamMeasure] + rw [arrayMeasure, Measure.snd_prod, streamMeasure] have : (fun ω ↦ ω n a) = (fun h : α → R ↦ h a) ∘ (fun ω : ℕ → α → R ↦ ω n) := rfl rw [this, ← Measure.map_map (by fun_prop) (by fun_prop), Measure.infinitePi_map_eval, Measure.infinitePi_map_eval] @@ -629,7 +575,7 @@ omit [DecidableEq α] [Nonempty α] [StandardBorelSpace α] in lemma indepFun_fst_add_one_aux (ν : Kernel α R) [IsMarkovKernel ν] (n : ℕ) : (fun ω ↦ ω.1 (n + 1)) ⟂ᵢ[arrayMeasure ν] (fun ω ↦ (fun (i : Iic n) ↦ ω.1 i, ω.2)) := by let μ₁ : Measure (ℕ → I) := Measure.infinitePi fun _ ↦ volume - let μ₂ : Measure (ℕ → α → R) := Bandit.streamMeasure ν + let μ₂ : Measure (ℕ → α → R) := streamMeasure ν -- Coordinates of μ₁ are independent have h_indep : iIndepFun (fun i (ω : ℕ → I) ↦ ω i) μ₁ := iIndepFun_infinitePi (fun _ ↦ measurable_id) @@ -1016,10 +962,10 @@ lemma hasCondDistrib_action' (alg : Algorithm α R) (ν : Kernel α R) [IsMarkov rw [h_indep'] congr simp only [arrayMeasure] - calc ((Measure.infinitePi fun x ↦ ℙ).prod (Bandit.streamMeasure ν)).map (fun ω ↦ ω.1 (n + 1)) + calc ((Measure.infinitePi fun x ↦ ℙ).prod (streamMeasure ν)).map (fun ω ↦ ω.1 (n + 1)) _ = (Measure.infinitePi fun x ↦ ℙ).map (Function.eval (n + 1)) := by nth_rw 2 [← Measure.fst_prod (μ := Measure.infinitePi fun x ↦ ℙ) - (ν := Bandit.streamMeasure ν)] + (ν := streamMeasure ν)] rw [Measure.fst, Measure.map_map (by fun_prop) (by fun_prop)] rfl _ = ℙ := by rw [Measure.infinitePi_map_eval] diff --git a/LeanBandits/Bandit/RewardByCountMeasure.lean b/LeanBandits/Bandit/RewardByCountMeasure.lean index 85b8aa46..bb0b4b35 100644 --- a/LeanBandits/Bandit/RewardByCountMeasure.lean +++ b/LeanBandits/Bandit/RewardByCountMeasure.lean @@ -20,7 +20,7 @@ variable {α Ω : Type*} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} [ {alg : Algorithm α ℝ} {ν : Kernel α ℝ} [IsMarkovKernel ν] {h_inter : IsAlgEnvSeq A R alg (stationaryEnv ν) P} -local notation "𝔓'" => P.prod (Bandit.streamMeasure ν) +local notation "𝔓'" => P.prod (streamMeasure ν) omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in lemma hasLaw_Z (a : α) (m : ℕ) : @@ -30,10 +30,10 @@ lemma hasLaw_Z (a : α) (m : ℕ) : _ = ((𝔓').snd).map (fun ω ↦ ω m a) := by rw [Measure.snd, Measure.map_map (by fun_prop) (by fun_prop)] rfl - _ = (Bandit.streamMeasure ν).map (fun ω ↦ ω m a) := by simp + _ = (streamMeasure ν).map (fun ω ↦ ω m a) := by simp _ = ((Measure.infinitePi fun _ ↦ Measure.infinitePi ν).map (fun ω ↦ ω m)).map (fun ω ↦ ω a) := by - rw [Bandit.streamMeasure, Measure.map_map (by fun_prop) (by fun_prop)] + rw [streamMeasure, Measure.map_map (by fun_prop) (by fun_prop)] rfl _ = ν a := by simp_rw [(measurePreserving_eval_infinitePi _ _).map_eq] @@ -44,9 +44,6 @@ notation "𝓛[" Y " | " X " in " s "; " μ "]" => Measure.map Y (μ[|X ⁻¹' s /-- Law of `Y` conditioned on the event that `X` equals `x`. -/ notation "𝓛[" Y " | " X " ← " x "; " μ "]" => Measure.map Y (μ[|X ⁻¹' {x}]) -local notation "𝔓t" => Bandit.trajMeasure alg ν -local notation "𝔓" => Bandit.measure alg ν - omit [DecidableEq α] in lemma condDistrib_reward'' [Countable α] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (n : ℕ) : @@ -107,7 +104,7 @@ lemma condIndepFun_reward_stepsUntil_action [StandardBorelSpace Ω] [Countable (fun ω ↦ R n ω.1) ({ω | stepsUntil A a m ω.1 = ↑n}.indicator (fun _ ↦ 1)) 𝔓' := by have hA := h.measurable_A have hR := h.measurable_R - exact condIndepFun_fst_prod (ν := Bandit.streamMeasure ν) + exact condIndepFun_fst_prod (ν := streamMeasure ν) (measurable_indicator_stepsUntil_eq hA hR a m n) (by fun_prop) (by fun_prop) (condIndepFun_reward_stepsUntil_action' h a m n) @@ -229,97 +226,8 @@ lemma identDistrib_rewardByCount_id [StandardBorelSpace Ω] [Countable α] lemma identDistrib_rewardByCount_eval [StandardBorelSpace Ω] [Countable α] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) (n m : ℕ) (hn : n ≠ 0) : - IdentDistrib (rewardByCount A R a n) (fun ω ↦ ω m a) 𝔓' (Bandit.streamMeasure ν) := + IdentDistrib (rewardByCount A R a n) (fun ω ↦ ω m a) 𝔓' (streamMeasure ν) := (identDistrib_rewardByCount_id h a n hn).trans (identDistrib_eval_eval_id_streamMeasure ν m a).symm --- lemma indepFun_rewardByCount_Iic [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] --- (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) --- (n : ℕ) : --- (rewardByCount A R a (n + 1)) ⟂ᵢ[𝔓'] fun ω (i : Iic n) ↦ rewardByCount A R a i ω := by --- sorry - --- lemma iIndepFun_rewardByCount' [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] --- (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) : --- iIndepFun (rewardByCount A R a) 𝔓' := by --- have hA := h.measurable_A --- have hR := h.measurable_R --- rw [iIndepFun_nat_iff_forall_indepFun (by fun_prop)] --- exact indepFun_rewardByCount_Iic h a - --- lemma iIndepFun_rewardByCount [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] --- (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) : --- iIndepFun (fun (p : α × ℕ) ↦ rewardByCount A R p.1 (p.2 + 1)) 𝔓' := by --- sorry - --- lemma identDistrib_rewardByCount_stream_all [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] --- (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) : --- IdentDistrib (fun ω (p : α × ℕ) ↦ rewardByCount A R p.1 (p.2 + 1) ω) --- (fun ω p ↦ ω p.2 p.1) 𝔓' (Bandit.streamMeasure ν) := by --- refine IdentDistrib.pi (fun p ↦ ?_) ?_ ?_ --- · refine identDistrib_rewardByCount_eval h p.1 (p.2 + 1) p.2 (by simp) (ν := ν) --- · exact iIndepFun_rewardByCount h --- · sorry - --- lemma identDistrib_rewardByCount_stream' [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] --- (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) : --- IdentDistrib (fun ω n ↦ rewardByCount A R a (n + 1) ω) (fun ω n ↦ ω n a) --- 𝔓' (Bandit.streamMeasure ν) := by --- refine IdentDistrib.pi (fun n ↦ ?_) ?_ ?_ --- · refine identDistrib_rewardByCount_eval h a (n + 1) n (by simp) (ν := ν) --- · have h_indep := iIndepFun_rewardByCount' h a --- exact iIndepFun.precomp (g := fun n ↦ n + 1) (fun i j hij ↦ by grind) h_indep --- · exact iIndepFun_eval_streamMeasure'' ν a - -omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in -lemma identDistrib_eval_streamMeasure_measure (a : α) : - IdentDistrib (fun ω n ↦ ω n a) (fun ω n ↦ ω.2 n a) - (Bandit.streamMeasure ν) 𝔓 := by - refine IdentDistrib.pi (fun n ↦ ?_) ?_ ?_ - · rw [← Bandit.snd_measure alg ν, Measure.snd, - identDistrib_map_left_iff (by fun_prop) (by fun_prop) - (Measurable.aemeasurable <| by fun_prop)] - exact IdentDistrib.refl (by fun_prop) - · exact iIndepFun_eval_streamMeasure'' ν a - · change iIndepFun (fun n ↦ ((fun ω ↦ ω n a) ∘ Prod.snd)) 𝔓 - rw [← iIndepFun_map_iff (by fun_prop) (fun _ ↦ Measurable.aemeasurable (by fun_prop))] - rw [← Measure.snd, Bandit.snd_measure] - exact iIndepFun_eval_streamMeasure'' ν a - --- lemma identDistrib_rewardByCount_stream [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] --- (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (a : α) : --- IdentDistrib (fun ω n ↦ rewardByCount A R a (n + 1) ω) (fun ω n ↦ ω.2 n a) 𝔓' 𝔓 := --- (identDistrib_rewardByCount_stream' h a).trans (identDistrib_eval_streamMeasure_measure a) - --- lemma indepFun_rewardByCount_of_ne [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] --- (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {a b : α} (hab : a ≠ b) : --- IndepFun (fun ω s ↦ rewardByCount A R a s ω) (fun ω s ↦ rewardByCount A R b s ω) 𝔓' := by --- sorry - --- lemma identDistrib_sum_Icc_rewardByCount [StandardBorelSpace Ω] [Nonempty Ω] [Countable α] --- (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) (m : ℕ) (a : α) : --- IdentDistrib (fun ω ↦ ∑ s ∈ Icc 1 m, rewardByCount A R a s ω) --- (fun ω ↦ ∑ s ∈ range m, ω.2 s a) 𝔓' 𝔓 := by --- have h1 (a : α) : --- IdentDistrib (fun ω s ↦ rewardByCount A R a (s + 1) ω) (fun ω s ↦ ω.2 s a) 𝔓' 𝔓 := --- identDistrib_rewardByCount_stream h a --- have h_eq (ω : Ω × (ℕ → α → ℝ)) : ∑ s ∈ Icc 1 m, rewardByCount A R a s ω --- = ∑ s ∈ range m, rewardByCount A R a (s + 1) ω := by --- let e : Icc 1 m ≃ range m := --- { 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] --- · simp --- · simp only [univ_eq_attach, mem_attach, forall_const, Subtype.forall, mem_Icc, --- forall_and_index] --- grind --- simp_rw [h_eq] --- exact IdentDistrib.comp (h1 a) (u := fun p ↦ ∑ s ∈ range m, p s) (by fun_prop) - end Bandits diff --git a/LeanBandits/Bandit/SumRewards.lean b/LeanBandits/Bandit/SumRewards.lean index 65ecf7e8..5a3822e4 100644 --- a/LeanBandits/Bandit/SumRewards.lean +++ b/LeanBandits/Bandit/SumRewards.lean @@ -57,7 +57,7 @@ lemma identDistrib_pullCount_prod_sum_Icc_rewardByCount' (n : ℕ) : IdentDistrib (fun ω a ↦ (pullCount A a n ω.1, ∑ i ∈ Icc 1 (pullCount A a n ω.1), rewardByCount A R a i ω)) (fun ω a ↦ (pullCount A a n ω, ∑ i ∈ Icc 1 (pullCount A a n ω), ω.2 (i - 1) a)) - ((𝔓).prod (Bandit.streamMeasure ν)) 𝔓 where + ((𝔓).prod (streamMeasure ν)) 𝔓 where aemeasurable_fst := by refine Measurable.aemeasurable ?_ rw [measurable_pi_iff] @@ -95,7 +95,7 @@ lemma identDistrib_pullCount_prod_sum_Icc_rewardByCount' (n : ℕ) : ∑ i ∈ Icc 1 (pullCount A a n ω.1), ω.1.2 (i - 1) a := Finset.sum_congr rfl fun i hi ↦ h_eq a i ω hi simp_rw [h_sum_eq] - conv_rhs => rw [← Measure.fst_prod (μ := 𝔓) (ν := Bandit.streamMeasure ν), + conv_rhs => rw [← Measure.fst_prod (μ := 𝔓) (ν := streamMeasure ν), Measure.fst] rw [AEMeasurable.map_map_of_aemeasurable _ (by fun_prop)] · rfl @@ -109,7 +109,7 @@ lemma identDistrib_pullCount_prod_sum_Icc_rewardByCount (n : ℕ) : IdentDistrib (fun ω a ↦ (pullCount A a n ω.1, ∑ i ∈ Icc 1 (pullCount A a n ω.1), rewardByCount A R a i ω)) (fun ω a ↦ (pullCount A a n ω, ∑ i ∈ range (pullCount A a n ω), ω.2 i a)) - ((𝔓).prod (Bandit.streamMeasure ν)) 𝔓 := by + ((𝔓).prod (streamMeasure ν)) 𝔓 := by convert identDistrib_pullCount_prod_sum_Icc_rewardByCount' n using 2 with ω rotate_left · infer_instance @@ -135,7 +135,7 @@ lemma identDistrib_pullCount_prod_sumRewards (n : ℕ) : (fun ω a ↦ (pullCount A a n ω, ∑ i ∈ range (pullCount A a n ω), ω.2 i a)) 𝔓 𝔓 := by suffices IdentDistrib (fun ω a ↦ (pullCount A a n ω.1, sumRewards A R a n ω.1)) (fun ω a ↦ (pullCount A a n ω, ∑ i ∈ range (pullCount A a n ω), ω.2 i a)) - ((𝔓).prod (Bandit.streamMeasure ν)) 𝔓 by + ((𝔓).prod (streamMeasure ν)) 𝔓 by -- todo: missing lemma about IdentDistrib? constructor · refine Measurable.aemeasurable ?_ @@ -145,7 +145,7 @@ lemma identDistrib_pullCount_prod_sumRewards (n : ℕ) : refine fun a ↦ Measurable.prod (by fun_prop) ?_ exact measurable_sum_range_of_le (n := n) (pullCount_le _ _) (by fun_prop) (by fun_prop) have h_eq := this.map_eq - nth_rw 1 [← Measure.fst_prod (μ := 𝔓) (ν := Bandit.streamMeasure ν), Measure.fst, + nth_rw 1 [← Measure.fst_prod (μ := 𝔓) (ν := streamMeasure ν), Measure.fst, Measure.map_map (by fun_prop) (by fun_prop)] exact h_eq simp_rw [← sum_rewardByCount_eq_sumRewards] @@ -191,19 +191,19 @@ lemma identDistrib_sumRewards_arm (a : α) (n : ℕ) : omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in lemma identDistrib_sum_range_snd (a : α) (k : ℕ) : IdentDistrib (fun ω ↦ ∑ i ∈ range k, ω.2 i a) (fun ω ↦ ∑ i ∈ range k, ω i a) - 𝔓 (Bandit.streamMeasure ν) where + 𝔓 (streamMeasure ν) where aemeasurable_fst := by fun_prop aemeasurable_snd := (measurable_sum _ fun i _ ↦ by fun_prop).aemeasurable map_eq := by rw [← Measure.snd_prod (μ := (Measure.infinitePi fun (_ : ℕ) ↦ (volume : Measure unitInterval))) - (ν := Bandit.streamMeasure ν), Measure.snd, Measure.map_map (by fun_prop) (by fun_prop)] + (ν := streamMeasure ν), Measure.snd, Measure.map_map (by fun_prop) (by fun_prop)] rfl lemma prob_pullCount_prod_sumRewards_mem_le (a : α) (n : ℕ) {s : Set (ℕ × ℝ)} [DecidablePred (· ∈ Prod.fst '' s)] (hs : MeasurableSet s) : 𝔓 {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - Bandit.streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by + streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by have h_ident := identDistrib_pullCount_prod_sumRewards_arm a n (ν := ν) (alg := alg) have : 𝔓 {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} = (𝔓).map (fun ω ↦ (pullCount A a n ω, sumRewards A R a n ω)) s := by @@ -223,10 +223,10 @@ lemma prob_pullCount_prod_sumRewards_mem_le (a : α) (n : ℕ) _ ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), 𝔓 {ω | ∑ i ∈ range k, ω.2 i a ∈ Prod.mk k ⁻¹' s} := measure_biUnion_finset_le _ _ _ = ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - (Bandit.streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by + (streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by congr with k have : (𝔓).map (fun ω ↦ ∑ i ∈ range k, ω.2 i a) = - (Bandit.streamMeasure ν).map (fun ω ↦ ∑ i ∈ range k, ω i a) := + (streamMeasure ν).map (fun ω ↦ ∑ i ∈ range k, ω i a) := (identDistrib_sum_range_snd a k).map_eq rw [Measure.ext_iff] at this specialize this (Prod.mk k ⁻¹' s) (hs.preimage (by fun_prop)) @@ -237,7 +237,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le (a : α) (n : ℕ) {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) {B : Set ℝ} (hB : MeasurableSet B) : 𝔓 {ω | pullCount A a n ω ∈ s ∧ sumRewards A R a n ω ∈ B} ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ s), - Bandit.streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by + streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by classical rcases Set.eq_empty_or_nonempty B with h_empty | h_nonempty · simp [h_empty] @@ -253,7 +253,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le (a : α) (n : ℕ) lemma prob_sumRewards_le_sumRewards_le [Fintype α] (a : α) (n m₁ m₂ : ℕ) : (𝔓) {ω | pullCount A (bestArm ν) n ω = m₁ ∧ pullCount A a n ω = m₂ ∧ sumRewards A R (bestArm ν) n ω ≤ sumRewards A R a n ω} ≤ - Bandit.streamMeasure ν + streamMeasure ν {ω | ∑ i ∈ range m₁, ω i (bestArm ν) ≤ ∑ i ∈ range m₂, ω i a} := by have h_ident := identDistrib_pullCount_prod_sumRewards_two_arms (bestArm ν) a n (ν := ν) (alg := alg) @@ -279,10 +279,10 @@ lemma prob_sumRewards_le_sumRewards_le [Fintype α] (a : α) (n m₁ m₂ : ℕ) refine measure_mono fun ω hω ↦ ?_ simp only [Set.preimage_setOf_eq, Set.mem_setOf_eq] at hω ⊢ grind - _ = Bandit.streamMeasure ν + _ = streamMeasure ν {ω | ∑ i ∈ range m₁, ω i (bestArm ν) ≤ ∑ i ∈ range m₂, ω i a} := by rw [← Measure.snd_prod (μ := (Measure.infinitePi fun (_ : ℕ) ↦ (volume : Measure unitInterval))) - (ν := Bandit.streamMeasure ν), Measure.snd, Measure.map_apply (by fun_prop)] + (ν := streamMeasure ν), Measure.snd, Measure.map_apply (by fun_prop)] · rfl simp only [measurableSet_setOf] fun_prop @@ -290,7 +290,7 @@ lemma prob_sumRewards_le_sumRewards_le [Fintype α] (a : α) (n m₁ m₂ : ℕ) lemma probReal_sumRewards_le_sumRewards_le [Fintype α] (a : α) (n m₁ m₂ : ℕ) : (𝔓).real {ω | pullCount A (bestArm ν) n ω = m₁ ∧ pullCount A a n ω = m₂ ∧ sumRewards A R (bestArm ν) n ω ≤ sumRewards A R a n ω} ≤ - (Bandit.streamMeasure ν).real + (streamMeasure ν).real {ω | ∑ i ∈ range m₁, ω i (bestArm ν) ≤ ∑ i ∈ range m₂, ω i a} := by simp_rw [measureReal_def] gcongr @@ -430,7 +430,7 @@ lemma prob_pullCount_prod_sumRewards_mem_le [Countable α] {s : Set (ℕ × ℝ)} [DecidablePred (· ∈ Prod.fst '' s)] (hs : MeasurableSet s) : P {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - Bandit.streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by + streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by have hA := h.measurable_A have hR := h.measurable_R calc P {ω | (pullCount A a n ω, sumRewards A R a n ω) ∈ s} @@ -444,7 +444,7 @@ lemma prob_pullCount_prod_sumRewards_mem_le [Countable α] sumRewards (ArrayModel.action alg) (ArrayModel.reward alg) a n ω) ∈ s} := by rw [Measure.map_apply (by fun_prop) hs]; rfl _ ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ Prod.fst '' s), - Bandit.streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := + streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := ArrayModel.prob_pullCount_prod_sumRewards_mem_le a n hs lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable α] @@ -452,7 +452,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable α] {s : Set ℕ} [DecidablePred (· ∈ s)] (hs : MeasurableSet s) {B : Set ℝ} (hB : MeasurableSet B) : P {ω | pullCount A a n ω ∈ s ∧ sumRewards A R a n ω ∈ B} ≤ ∑ k ∈ (range (n + 1)).filter (· ∈ s), - Bandit.streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by + streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by classical rcases Set.eq_empty_or_nonempty B with h_empty | h_nonempty · simp [h_empty] @@ -468,7 +468,7 @@ lemma prob_pullCount_mem_and_sumRewards_mem_le [Countable α] lemma prob_sumRewards_mem_le [Countable α] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {B : Set ℝ} (hB : MeasurableSet B) : P (sumRewards A R a n ⁻¹' B) ≤ - ∑ k ∈ range (n + 1), Bandit.streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by + ∑ k ∈ range (n + 1), streamMeasure ν {ω | ∑ i ∈ range k, ω i a ∈ B} := by classical have h_le := prob_pullCount_mem_and_sumRewards_mem_le h .univ hB (a := a) (n := n) simpa using h_le @@ -477,7 +477,7 @@ lemma prob_pullCount_eq_and_sumRewards_mem_le [Countable α] (h : IsAlgEnvSeq A R alg (stationaryEnv ν) P) {m : ℕ} (hm : m ≤ n) {B : Set ℝ} (hB : MeasurableSet B) : P {ω | pullCount A a n ω = m ∧ sumRewards A R a n ω ∈ B} ≤ - Bandit.streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B} := by + streamMeasure ν {ω | ∑ i ∈ range m, ω i a ∈ B} := by have h_le := prob_pullCount_mem_and_sumRewards_mem_le h (s := {m}) (by simp) hB (a := a) (n := n) have hm' : m < n + 1 := by lia simpa [hm'] using h_le @@ -486,7 +486,7 @@ lemma probReal_sumRewards_le_sumRewards_le [Fintype α] (h : IsAlgEnvSeq A R alg (a : α) (n m₁ m₂ : ℕ) : P.real {ω | pullCount A (bestArm ν) n ω = m₁ ∧ pullCount A a n ω = m₂ ∧ sumRewards A R (bestArm ν) n ω ≤ sumRewards A R a n ω} ≤ - (Bandit.streamMeasure ν).real + (streamMeasure ν).real {ω | ∑ i ∈ range m₁, ω i (bestArm ν) ≤ ∑ i ∈ range m₂, ω i a} := by have hA := h.measurable_A have hR := h.measurable_R @@ -519,7 +519,7 @@ section Subgaussian omit [DecidableEq α] [StandardBorelSpace α] in lemma probReal_sum_le_sum_streamMeasure [Fintype α] (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) (a : α) (m : ℕ) : - (Bandit.streamMeasure ν).real + (streamMeasure ν).real {ω | ∑ s ∈ range m, ω s (bestArm ν) ≤ ∑ s ∈ range m, ω s a} ≤ Real.exp (-↑m * gap ν a ^ 2 / 4) := by by_cases ha : a = bestArm ν @@ -551,11 +551,11 @@ omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in lemma prob_sum_le_sqrt_log (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) {c : ℝ} (hc : 0 ≤ c) (a : α) (k : ℕ) (hk : k ≠ 0) : - Bandit.streamMeasure ν + streamMeasure ν {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(c * k * Real.log (n + 1))} ≤ 1 / (n + 1) ^ (c / 2) := by calc - Bandit.streamMeasure ν + streamMeasure ν {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(c * k * Real.log (n + 1))} _ ≤ ENNReal.ofReal (Real.exp (-(√(c * k * Real.log (n + 1))) ^ 2 / (2 * k * 1))) := by rw [← ofReal_measureReal] @@ -581,11 +581,11 @@ omit [DecidableEq α] [StandardBorelSpace α] [Nonempty α] in lemma prob_sum_ge_sqrt_log (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) {c : ℝ} (hc : 0 ≤ c) (a : α) (k : ℕ) (hk : k ≠ 0) : - Bandit.streamMeasure ν + streamMeasure ν {ω | √(c * k * Real.log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} ≤ 1 / (n + 1) ^ (c / 2) := by calc - Bandit.streamMeasure ν + streamMeasure ν {ω | √(c * k * Real.log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} _ ≤ ENNReal.ofReal (Real.exp (-(√(c * k * Real.log (n + 1))) ^ 2 / (2 * k * 1))) := by rw [← ofReal_measureReal] diff --git a/LeanBandits/BanditAlgorithms/ETC.lean b/LeanBandits/BanditAlgorithms/ETC.lean index 14445cd2..803202c6 100644 --- a/LeanBandits/BanditAlgorithms/ETC.lean +++ b/LeanBandits/BanditAlgorithms/ETC.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne import LeanBandits.Bandit.SumRewards import LeanBandits.BanditAlgorithms.AuxSums import LeanBandits.ForMathlib.MeasurableArgMax +import LeanBandits.SequentialLearning.Deterministic /-! # The Explore-Then-Commit Algorithm diff --git a/LeanBandits/BanditAlgorithms/UCB.lean b/LeanBandits/BanditAlgorithms/UCB.lean index 121bb0e8..f19c5a2b 100644 --- a/LeanBandits/BanditAlgorithms/UCB.lean +++ b/LeanBandits/BanditAlgorithms/UCB.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne import LeanBandits.Bandit.SumRewards import LeanBandits.BanditAlgorithms.AuxSums import LeanBandits.ForMathlib.MeasurableArgMax +import LeanBandits.SequentialLearning.Deterministic /-! # UCB algorithm @@ -216,18 +217,18 @@ lemma pullCount_arm_le [Nonempty (Fin K)] (hc : 0 ≤ c) lemma todo (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) (hc : 0 ≤ c) (a : Fin K) (n k : ℕ) (hk : k ≠ 0) : - Bandit.streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(c * log (n + 1) / k) ≤ (ν a)[id]} ≤ + streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(c * log (n + 1) / k) ≤ (ν a)[id]} ≤ 1 / (n + 1) ^ (c / 2) := by have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp) - calc Bandit.streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(c * log (n + 1) / k) ≤ (ν a)[id]} - _ = Bandit.streamMeasure ν + calc streamMeasure ν {ω | (∑ m ∈ range k, ω m a) / k + √(c * log (n + 1) / k) ≤ (ν a)[id]} + _ = streamMeasure ν {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) / k ≤ - √(c * log (n + 1) / k)} := by congr with ω field_simp rw [Finset.sum_sub_distrib] simp grind - _ = Bandit.streamMeasure ν + _ = streamMeasure ν {ω | (∑ s ∈ range k, (ω s a - (ν a)[id])) ≤ - √(c * k * log (n + 1))} := by congr with ω field_simp @@ -238,19 +239,19 @@ lemma todo (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) lemma todo' (hν : ∀ a, HasSubgaussianMGF (fun x ↦ x - (ν a)[id]) 1 (ν a)) (hc : 0 ≤ c) (a : Fin K) (n k : ℕ) (hk : k ≠ 0) : - Bandit.streamMeasure ν + streamMeasure ν {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(c * log (n + 1) / k)} ≤ 1 / (n + 1) ^ (c / 2) := by have h_log_nonneg : 0 ≤ log (n + 1) := log_nonneg (by simp) - calc Bandit.streamMeasure ν {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(c * log (n + 1) / k)} - _ = Bandit.streamMeasure ν + calc streamMeasure ν {ω | (ν a)[id] ≤ (∑ m ∈ range k, ω m a) / k - √(c * log (n + 1) / k)} + _ = streamMeasure ν {ω | √(c * log (n + 1) / k) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id])) / k} := by congr with ω field_simp rw [Finset.sum_sub_distrib] simp grind - _ = Bandit.streamMeasure ν + _ = streamMeasure ν {ω | √(c * k * log (n + 1)) ≤ (∑ s ∈ range k, (ω s a - (ν a)[id]))} := by congr with ω field_simp @@ -272,15 +273,15 @@ lemma prob_ucbIndex_le [Nonempty (Fin K)] classical calc P {h | 0 < pullCount A a n h ∧ empMean A R a n h + ucbWidth A c a n h ≤ (ν a)[id]} _ ≤ ∑ k ∈ range (n + 1) with k ∈ Prod.fst '' s, - (Bandit.streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := + (streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := prob_pullCount_prod_sumRewards_mem_le h hs _ ≤ ∑ k ∈ Icc 1 n, - (Bandit.streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by + (streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by refine Finset.sum_le_sum_of_subset_of_nonneg (fun m ↦ ?_) fun _ _ _ ↦ by positivity simp [s] grind _ = ∑ k ∈ Icc 1 n, - (Bandit.streamMeasure ν) {ω | (∑ i ∈ range k, ω i a) / k + √(c * log (↑n + 1) / k) ≤ + (streamMeasure ν) {ω | (∑ i ∈ range k, ω i a) / k + √(c * log (↑n + 1) / k) ≤ (ν a)[id]} := by refine Finset.sum_congr rfl fun k hk ↦ ?_ congr with ω @@ -312,15 +313,15 @@ lemma prob_ucbIndex_ge [Nonempty (Fin K)] classical calc P {h | 0 < pullCount A a n h ∧ (ν a)[id] ≤ empMean A R a n h - ucbWidth A c a n h} _ ≤ ∑ k ∈ range (n + 1) with k ∈ Prod.fst '' s, - (Bandit.streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := + (streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := prob_pullCount_prod_sumRewards_mem_le h hs _ ≤ ∑ k ∈ Icc 1 n, - (Bandit.streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by + (streamMeasure ν) {ω | ∑ i ∈ range k, ω i a ∈ Prod.mk k ⁻¹' s} := by refine Finset.sum_le_sum_of_subset_of_nonneg (fun m ↦ ?_) fun _ _ _ ↦ by positivity simp [s] grind _ = ∑ k ∈ Icc 1 n, - (Bandit.streamMeasure ν) + (streamMeasure ν) {ω | (ν a)[id] ≤ (∑ i ∈ range k, ω i a) / k - √(c * log (↑n + 1) / k)} := by refine Finset.sum_congr rfl fun k hk ↦ ?_ congr with ω diff --git a/blueprint/lean_decls b/blueprint/lean_decls index ced961f0..ce50c4fb 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -51,8 +51,6 @@ Learning.rewardByCount_pullCount_add_one_eq_reward Learning.sumRewards Learning.empMean Learning.sum_rewardByCount_eq_sumRewards -Bandits.Bandit.trajMeasure -Bandits.Bandit.measure Bandits.ArrayModel.probSpace Bandits.ArrayModel.arrayMeasure Bandits.ArrayModel.algFunction diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index b304f593..68f7ff9d 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -22,17 +22,6 @@ \section{Algorithm, bandit and probability space} \item the history is updated to $H_{t+1} = ((A_0, R_0), \ldots, (A_{t+1}, R_{t+1}))$. \end{itemize} -We now want to define a probability space on which we can study the sequences of arms and rewards, and formulate probabilistic statements about the interaction between the algorithm and the bandit. - - -\begin{definition}[Bandit probability space]\label{def:Bandit.measure} - \uses{def:stationaryEnv,def:environment,def:algorithm,def:trajMeasure} - \leanok - \lean{Bandits.Bandit.trajMeasure, Bandits.Bandit.measure} -As in Definition~\ref{def:trajMeasure}, an algorithm $(\pi, P_0)$ and bandit $\nu$ together defines a probability distribution $\mathbb{P}_{\mathcal{T}}$ on the space $\Omega_{\mathcal{T}} := (\mathcal{A} \times \mathbb{R})^{\mathbb{N}}$, the space of infinite sequences of arms and rewards. -We augment that probability space with a stream of rewards from each arm, independent of the bandit interaction, to get the probability space $(\Omega, \mathbb{P})$, where $\Omega = \Omega_{\mathcal{T}} \times \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$ and $\mathbb{P} = \mathbb{P}_{\mathcal{T}} \otimes (\bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a))$. -\end{definition} - \section{The array model of rewards}