Blueprint update

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 _ ↦ α × ℝ)

LeanBandits/Regret.lean

@@ -66,26 +66,27 @@ 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
   · simp [pullCount]
   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 : ℕ) :

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)

blueprint/lean_decls

@@ -8,4 +8,10 @@ Bandits.condDistrib_arm
 Bandits.regret
 Bandits.gap
 Bandits.pullCount
-Bandits.regret_eq_sum_pullCount_mul_gap
+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

blueprint/src/chapters/bandit.tex

@@ -140,13 +140,17 @@ \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}
 
 
 \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}
@@ -163,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}
@@ -175,30 +179,36 @@ \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}
+\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}
 
 
 \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}
 
-\begin{proof}
+\begin{proof}\leanok
 
 \end{proof}
 
 
 \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}
+\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$.
 
@@ -207,12 +217,14 @@ \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
   \: .
 \end{align*}
 \end{lemma}
 
-\begin{proof}
+\begin{proof}\leanok
 
 \end{proof}

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"]]
+[]