From 4bc8d95e3176245b920c012f3a9d6e333a93ea56 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 2 Sep 2025 14:23:28 +0200 Subject: [PATCH 1/2] blueprint update --- LeanBandits/Bandit.lean | 4 ++++ LeanBandits/Regret.lean | 9 +++++---- LeanBandits/UCB.lean | 3 +++ blueprint/lean_decls | 8 +++++++- blueprint/src/chapters/bandit.tex | 16 ++++++++++++++-- scripts/nolints.json | 7 +------ 6 files changed, 34 insertions(+), 13 deletions(-) diff --git a/LeanBandits/Bandit.lean b/LeanBandits/Bandit.lean index af135bfd..1c58fb5f 100644 --- a/LeanBandits/Bandit.lean +++ b/LeanBandits/Bandit.lean @@ -76,10 +76,13 @@ noncomputable def trajMeasure (b : Bandit α) : Measure (ℕ → α × ℝ) := (b.traj 0) ∘ₘ ((b.p0 ⊗ₘ b.ν).map (MeasurableEquiv.piIicZero _).symm) +/-- Measure of an infinite stream of rewards from each arm. -/ noncomputable def streamMeasure (b : Bandit α) : Measure (ℕ → α → ℝ) := Measure.infinitePi fun _ ↦ Measure.infinitePi b.ν +/-- Joint distribution of the sequence of arm pulled and rewards, and a stream of independent +rewards from all arms. -/ noncomputable def measure (b : Bandit α) : Measure ((ℕ → α × ℝ) × (ℕ → α → ℝ)) := (b.trajMeasure).prod (b.streamMeasure) @@ -112,6 +115,7 @@ def reward (n : ℕ) (h : ℕ → α × ℝ) : ℝ := (h n).2 `ℕ → α × ℝ`. -/ def hist (n : ℕ) (h : ℕ → α × ℝ) : Iic n → α × ℝ := fun i ↦ h i +/-- Filtration of the bandit process. -/ def ℱ (α : Type*) [MeasurableSpace α] : Filtration ℕ (inferInstance : MeasurableSpace (ℕ → α × ℝ)) := MeasureTheory.Filtration.piLE (X := fun _ ↦ α × ℝ) diff --git a/LeanBandits/Regret.lean b/LeanBandits/Regret.lean index 516ce365..8a5b4c9e 100644 --- a/LeanBandits/Regret.lean +++ b/LeanBandits/Regret.lean @@ -66,18 +66,19 @@ lemma stepsUntil_pullCount_eq (k : ℕ → α) (t : ℕ) : simpa [stepsUntil, pullCount_eq_pullCount_add_one] exact fun t' h ↦ Nat.le_of_lt_succ ((monotone_pullCount k (k t)).reflect_lt (h ▸ lt_add_one _)) +/-- Reward obtained when pulling arm `a` for the `m`-th time. -/ noncomputable def rewardByCount (a : α) (m : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) : ℝ := match (stepsUntil (arm · h) a m) with | ⊤ => z m a | (n : ℕ) => reward n h -lemma rewardByCount_of_pullCount_add_one_eq_reward (t : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) : +lemma rewardByCount_pullCount_add_one_eq_reward (t : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) : rewardByCount (arm t h) (pullCount (arm · h) (arm t h) t + 1) h z = reward t h := by rw [rewardByCount, ← pullCount_eq_pullCount_add_one, stepsUntil_pullCount_eq] -open Classical in -lemma sum_rewardByCount_eq_sum_reward (a : α) (t : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) : +lemma sum_rewardByCount_eq_sum_reward [DecidableEq α] + (a : α) (t : ℕ) (h : ℕ → α × ℝ) (z : ℕ → α → ℝ) : ∑ m ∈ Icc 1 (pullCount (arm · h) a t), rewardByCount a m h z = ∑ s ∈ range t, if (arm s h) = a then (reward s h) else 0 := by induction' t with t ht @@ -85,7 +86,7 @@ lemma sum_rewardByCount_eq_sum_reward (a : α) (t : ℕ) (h : ℕ → α × ℝ) by_cases hta : arm t h = a · rw [← hta] at ht ⊢ rw [pullCount_eq_pullCount_add_one, sum_Icc_succ_top (Nat.le_add_left 1 _), ht] - rw [sum_range_succ, if_pos rfl, rewardByCount_of_pullCount_add_one_eq_reward] + rw [sum_range_succ, if_pos rfl, rewardByCount_pullCount_add_one_eq_reward] · rwa [pullCount_eq_pullCount _ _ _ hta, sum_range_succ, if_neg hta, add_zero] lemma sum_pullCount_mul [Fintype α] (k : ℕ → α) (f : α → ℝ) (t : ℕ) : diff --git a/LeanBandits/UCB.lean b/LeanBandits/UCB.lean index 98868d85..9abcc2c4 100644 --- a/LeanBandits/UCB.lean +++ b/LeanBandits/UCB.lean @@ -20,8 +20,11 @@ variable {α : Type*} {mα : MeasurableSpace α} {ν : Kernel α ℝ} {k : ℕ variable [Fintype α] [Nonempty α] {c : ℝ} {μ : α → ℝ} {N : α → ℕ} {a : α} +/-- The exploration bonus of the UCB algorithm, which corresponds to the width of +a confidence interval. -/ noncomputable def ucbWidth (c : ℝ) (N : α → ℕ) (t : ℕ) (a : α) : ℝ := √(c * log t / N a) +/-- The arm pulled by the UCB algorithm. -/ noncomputable def ucbArm (c : ℝ) (μ : α → ℝ) (N : α → ℕ) (t : ℕ) : α := (exists_max_image univ (fun a ↦ μ a + ucbWidth c N t a) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index f8c5653e..42268093 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -8,4 +8,10 @@ Bandits.condDistrib_arm Bandits.regret Bandits.gap Bandits.pullCount -Bandits.regret_eq_sum_pullCount_mul_gap \ No newline at end of file +Bandits.regret_eq_sum_pullCount_mul_gap +Bandits.stepsUntil +Bandits.rewardByCount +Bandits.stepsUntil_pullCount_le +Bandits.stepsUntil_pullCount_eq +Bandits.rewardByCount_pullCount_add_one_eq_reward +Bandits.sum_rewardByCount_eq_sum_reward \ No newline at end of file diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 0e457562..40c1d2d4 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -140,6 +140,8 @@ \section{Alternative model} \begin{definition}\label{def:timeOfPull} \uses{def:pullCount} + \leanok + \lean{Bandits.stepsUntil} For an arm $a \in \mathcal{A}$ and a time $n \in \mathbb{N}$, we denote by $T_{n,a}$ the time at which arm $a$ was pulled for the $n$-th time, that is $T_{n,a} = \min\{s \in \mathbb{N} \mid N_{s+1,a} = n\}$. Note that $T_{n, a}$ can be infinite if the arm is not pulled $n$ times. \end{definition} @@ -147,6 +149,8 @@ \section{Alternative model} \begin{definition}\label{def:altReward} \uses{def:timeOfPull} + \leanok + \lean{Bandits.rewardByCount} For $a \in \mathcal{A}$ and $n \in \mathbb{N}$, let $Z_{n,a} \sim \nu(a)$, independent of everything else. We define $Y_{n, a} = X_{T_{n,a}} \mathbb{I}\{T_{n, a} < \infty\} + Z_{n,a} \mathbb{I}\{T_{n, a} = \infty\}$, the reward received when pulling arm $a$ for the $n$-th time if that time is finite, and equal to $Z_{n,a}$ otherwise. \end{definition} @@ -175,7 +179,9 @@ \section{Alternative model} \begin{lemma}\label{lem:timeOfPull_pullCount_le} \uses{def:timeOfPull,def:pullCount} -$T_{N_{t, a}, a} \le t - 1 < \infty$ for all $t \in \mathbb{N}$ and $a \in \mathcal{A}$. + \leanok + \lean{Bandits.stepsUntil_pullCount_le} +$T_{N_{t+1, a}, a} \le t < \infty$ for all $t \in \mathbb{N}$ and $a \in \mathcal{A}$. \end{lemma} \begin{proof} @@ -185,6 +191,8 @@ \section{Alternative model} \begin{lemma}\label{lem:timeOfPull_pullCount_eq} \uses{def:timeOfPull,def:pullCount} + \leanok + \lean{Bandits.stepsUntil_pullCount_eq} $T_{N_{t+1, A_t}, A_t} = t$ for all $t \in \mathbb{N}$. \end{lemma} @@ -195,7 +203,9 @@ \section{Alternative model} \begin{lemma}\label{lem:altReward_pullCount} \uses{def:altReward,def:pullCount} -$Y_{N_{t+1,A_t}, A_t} = X_t$ for all $t \in \mathbb{N}$ and $a \in \mathcal{A}$. + \leanok + \lean{Bandits.rewardByCount_pullCount_add_one_eq_reward} +$Y_{N_{t+1, A_t}, A_t} = X_t$ for all $t \in \mathbb{N}$ and $a \in \mathcal{A}$. \end{lemma} \begin{proof} @@ -207,6 +217,8 @@ \section{Alternative model} \begin{lemma}\label{lem:sum_altReward} \uses{def:altReward,def:pullCount} + \leanok + \lean{Bandits.sum_rewardByCount_eq_sum_reward} \begin{align*} \sum_{n=1}^{N_{t, a}} Y_{n, a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\} X_s \: . diff --git a/scripts/nolints.json b/scripts/nolints.json index 9d61646d..fe51488c 100644 --- a/scripts/nolints.json +++ b/scripts/nolints.json @@ -1,6 +1 @@ -[["docBlame", "Bandits.rewardByCount"], - ["docBlame", "Bandits.ucbArm"], - ["docBlame", "Bandits.ucbWidth"], - ["docBlame", "Bandits.ℱ"], - ["docBlame", "Bandits.Bandit.measure"], - ["docBlame", "Bandits.Bandit.streamMeasure"]] +[] From 5f3be20493b1bc775ac677dbeac6bb3adfe9c5f3 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Tue, 2 Sep 2025 14:27:52 +0200 Subject: [PATCH 2/2] leanok for proofs --- blueprint/src/chapters/bandit.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 40c1d2d4..bfcc57fb 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -167,7 +167,7 @@ \section{Alternative model} \end{proof} -\begin{lemma}\label{lem:indepednent_altReward} +\begin{lemma}\label{lem:independent_altReward} \uses{def:altReward} For $a \in \mathcal{A}$, let $Y^{(a)} = (Y_{n,a})_{n \in \mathbb{N}} \in \mathbb{R}^{\mathbb{N}}$ be the sequence of rewards obtained from pulling arm $a$. Then the sequences $(Y^{(a)})_{a \in \mathcal{A}}$ are independent. \end{lemma} @@ -184,7 +184,7 @@ \section{Alternative model} $T_{N_{t+1, a}, a} \le t < \infty$ for all $t \in \mathbb{N}$ and $a \in \mathcal{A}$. \end{lemma} -\begin{proof} +\begin{proof}\leanok By definition, $T_{N_{t,a}, a} = \min\{s \in \mathbb{N} \mid N_{s+1,a} = N_{t,a}\} \le t - 1 < \infty$. \end{proof} @@ -196,7 +196,7 @@ \section{Alternative model} $T_{N_{t+1, A_t}, A_t} = t$ for all $t \in \mathbb{N}$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \end{proof} @@ -208,7 +208,7 @@ \section{Alternative model} $Y_{N_{t+1, A_t}, A_t} = X_t$ for all $t \in \mathbb{N}$ and $a \in \mathcal{A}$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \uses{lem:timeOfPull_pullCount_eq} By Lemma~\ref{lem:timeOfPull_pullCount_eq}, we have $T_{N_{t+1,A_t}, A_t} = t < \infty$, so $Y_{N_{t+1,A_t}, A_t} = X_{T_{N_{t+1,A_t}, A_t}} = X_t$. @@ -225,6 +225,6 @@ \section{Alternative model} \end{align*} \end{lemma} -\begin{proof} +\begin{proof}\leanok \end{proof}