From 495d772a4b7614e964d53609c7aa2f6dd0699021 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Sun, 18 Jan 2026 14:28:47 +0100 Subject: [PATCH] update uses --- blueprint/src/chapters/algorithm.tex | 44 ++++---- blueprint/src/chapters/bandit.tex | 123 ++++++++++++----------- blueprint/src/chapters/concentration.tex | 18 ++-- blueprint/src/chapters/etc.tex | 15 +-- blueprint/src/chapters/ucb.tex | 26 ++--- 5 files changed, 122 insertions(+), 104 deletions(-) diff --git a/blueprint/src/chapters/algorithm.tex b/blueprint/src/chapters/algorithm.tex index bc7d5acb..13552567 100644 --- a/blueprint/src/chapters/algorithm.tex +++ b/blueprint/src/chapters/algorithm.tex @@ -77,7 +77,7 @@ \chapter{Iterative stochastic algorithms} \begin{definition}[Algorithm-environment interaction]\label{def:IsAlgEnvSeq} - \uses{def:algorithm, def:environment} + \uses{def:environment,def:algorithm,def:history} \leanok \lean{Learning.IsAlgEnvSeq} Let $\mathfrak{A}$ be an algorithm as in Definition~\ref{def:algorithm} and $\mathfrak{E}$ be an environment as in Definition~\ref{def:environment}. @@ -100,7 +100,7 @@ \chapter{Iterative stochastic algorithms} \begin{lemma}\label{lem:law_step} - \uses{def:IsAlgEnvSeq, def:history} + \uses{def:environment,def:IsAlgEnvSeq,def:algorithm,def:history} \leanok \lean{Learning.IsAlgEnvSeq.hasLaw_step_zero, Learning.IsAlgEnvSeq.hasCondDistrib_step} In an algorithm-environment interaction $(A, R, P)$ as in Definition~\ref{def:IsAlgEnvSeq}, @@ -116,7 +116,7 @@ \chapter{Iterative stochastic algorithms} \begin{definition}\label{def:IsAlgEnvSeq.filtration} - \uses{def:IsAlgEnvSeq, def:history} + \uses{def:history} \leanok \lean{Learning.IsAlgEnvSeq.filtration, Learning.IsAlgEnvSeq.filtrationAction} For an algorithm-environment interaction $(A, R, P)$ as in Definition~\ref{def:IsAlgEnvSeq}, we denote by $\mathcal{F}_t$ the sigma-algebra generated by the history up to time $t$: $\mathcal{F}_t = \sigma(H_t)$. @@ -125,13 +125,14 @@ \chapter{Iterative stochastic algorithms} \begin{theorem}[\cite{lattimore2020bandit}, Proposition 4.8]\label{thm:isAlgEnvSeq_unique} - \uses{def:IsAlgEnvSeq} + \uses{def:environment,def:IsAlgEnvSeq,def:algorithm} \leanok \lean{Learning.isAlgEnvSeq_unique} If $(A, R, P)$ and $(A', R', P')$ are two algorithm-environment interactions for the same algorithm $\mathfrak{A}$ and environment $\mathfrak{E}$, then the joint distributions of the sequences of actions and observations are equal: the law of $(A_i, R_i)_{i \in \mathbb{N}}$ under $P$ is equal to the law of $(A'_i, R'_i)_{i \in \mathbb{N}}$ under $P'$. \end{theorem} \begin{proof}\leanok + \uses{thm:ionescu-tulcea,lem:law_step,def:trajMeasure} \end{proof} @@ -144,20 +145,20 @@ \section{Stationary environment} Let $(A, R, P)$ be an algorithm-environment interaction in a stationary environment with kernel $\nu$. \begin{lemma}\label{lem:condDistrib_reward_stationaryEnv} - \uses{def:IsAlgEnvSeq, def:stationaryEnv} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm} \leanok \lean{Learning.IsAlgEnvSeq.condDistrib_reward_stationaryEnv} In a stationary environment, for any $t \in \mathbb{N}$, the conditional distribution $P\left[R_t \mid A_t\right]$ is $(A_{t*} P_{\mathcal{T}})$-almost surely equal to $\nu$. \end{lemma} \begin{proof}\leanok - \uses{lem:law_step, def:stationaryEnv} + \uses{def:environment,lem:law_step,def:history} \end{proof} \begin{lemma}\label{lem:condIndepFun_reward_hist_action} - \uses{def:IsAlgEnvSeq, def:stationaryEnv} + \uses{def:stationaryEnv,def:environment,def:IsAlgEnvSeq,def:algorithm,def:history} \leanok \lean{Learning.IsAlgEnvSeq.condIndepFun_reward_hist_action} In a stationary environment, for any $t \in \mathbb{N}$, the reward $R_{t+1}$ is conditionally independent of the history $H_t$ given the action $A_{t+1}$ (more succinctly, $R_{t+1} \ind H_t \mid A_{t+1}$). @@ -244,7 +245,7 @@ \subsection{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:IT.condDistrib_X_add_one} - \uses{def:IT.history, def:trajMeasure} + \uses{def:IT.history, thm:ionescu-tulcea, def:trajMeasure} \leanok \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure} For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t$. @@ -304,28 +305,28 @@ \subsection{Case of an algorithm-environment interaction} We need to check that the random variables $A_t$ and $R_t$ have the expected conditional distributions. \begin{lemma}\label{lem:IT.condDistrib_A_add_one} - \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment} + \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure,def:IT.history} \leanok \lean{Learning.IT.condDistrib_action} For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right] = \pi_t$. \end{lemma} \begin{proof}\leanok - \uses{lem:IT.condDistrib_X_add_one} + \uses{lem:IT.condDistrib_X_add_one,def:IT.history} By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right] = \kappa_t = \pi_t \otimes \nu_t$. Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}$, $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to the projection of $\kappa_t$ on $\mathcal{A}$, which is $\pi_t$. \end{proof} \begin{lemma}\label{lem:IT.condDistrib_R_add_one} - \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment} + \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure,def:IT.history} \leanok \lean{Learning.IT.condDistrib_reward} For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left[R_{t+1} \mid H_t, A_{t+1}\right] = \nu_t$. \end{lemma} \begin{proof}\leanok - \uses{lem:IT.condDistrib_X_add_one, lem:IT.condDistrib_A_add_one} + \uses{lem:IT.condDistrib_X_add_one,def:IT.history,lem:IT.condDistrib_A_add_one} It suffices to show that $((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t = (H_t, A_{t+1}, R_{t+1})_* P_{\mathcal{T}} = (H_t, X_{t+1})_* P_{\mathcal{T}}$. By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right] = \pi_t \otimes \nu_t$. Thus $((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = (H_t, X_{t+1})_* P_{\mathcal{T}}$. @@ -337,27 +338,27 @@ \subsection{Case of an algorithm-environment interaction} \begin{lemma}\label{lem:IT.law_A_zero} - \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment} + \uses{def:environment,def:algorithm,def:IT.actionReward,def:trajMeasure} \leanok \lean{Learning.IT.hasLaw_action_zero} The law of $A_0$ under $P_{\mathcal{T}}$ is $P_0$. \end{lemma} \begin{proof}\leanok - \uses{lem:IT.law_X_zero} + \uses{thm:ionescu-tulcea,def:IT.history,lem:IT.law_X_zero} $X_0$ has law $\mu = P_0 \otimes \nu'_0$. $A_0$ is the projection of $X_0$ on the first space $\mathcal{A}$ and $\nu_0'$ is Markov, so $A_0$ has law $P_0$. \end{proof} \begin{lemma}\label{lem:IT.condDistrib_R_zero} - \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment} + \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure} \leanok \lean{Learning.IT.condDistrib_reward_zero} $P_{\mathcal{T}}\left[R_0 \mid A_0\right] = \nu'_0$. \end{lemma} \begin{proof}\leanok - \uses{lem:IT.law_X_zero} + \uses{lem:IT.law_X_zero,lem:IT.law_A_zero,def:IT.history} To prove almost sure equality, it is enough to prove that $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left[R_0 \mid A_0\right] = (A_{0*} P_{\mathcal{T}}) \otimes \nu'_0$. By definition of the conditional distribution, we have $(A_{0*} P_{\mathcal{T}}) \otimes P_{\mathcal{T}}\left[R_0 \mid A_0\right] = (A_0, R_0)_* P_{\mathcal{T}} = X_{0*} P_{\mathcal{T}}$. By Lemma~\ref{lem:IT.law_X_zero}, $X_{0*} P_{\mathcal{T}} = \mu = P_0 \otimes \nu'_0$. @@ -367,14 +368,14 @@ \subsection{Case of an algorithm-environment interaction} \begin{theorem}\label{thm:isAlgEnvSeq_trajMeasure} - \uses{def:IsAlgEnvSeq, def:trajMeasure} + \uses{def:environment,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure} \leanok \lean{Learning.IT.isAlgEnvSeq_trajMeasure} In the probability space $(\Omega_{\mathcal{T}}, P_{\mathcal{T}})$ constructed from an algorithm $\mathfrak{A}$ and an environment $\mathfrak{E}$ as above, the sequences of random variables $A : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{A}$ and $R : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{R}$ form an algorithm-environment interaction for $\mathfrak{A}$ and $\mathfrak{E}$. \end{theorem} \begin{proof}\leanok - \uses{lem:IT.law_A_zero, lem:IT.condDistrib_R_zero, lem:IT.condDistrib_A_add_one, lem:IT.condDistrib_R_add_one} + \uses{def:history,lem:IT.law_A_zero,lem:IT.condDistrib_R_zero,lem:IT.condDistrib_A_add_one,lem:IT.condDistrib_R_add_one} The four conditions of Definition~\ref{def:IsAlgEnvSeq} are exactly the statements of Lemmas~\ref{lem:IT.law_A_zero}, \ref{lem:IT.condDistrib_R_zero}, \ref{lem:IT.condDistrib_A_add_one} and \ref{lem:IT.condDistrib_R_add_one}. \end{proof} @@ -386,7 +387,6 @@ \section{Finitely many actions} We can also define the time step at which an action was chosen a certain number of times, and the value of the reward obtained when pulling an action for the $m$-th time. \begin{definition}[Pull counts]\label{def:pullCount} - \uses{def:IT.actionReward} \leanok \lean{Learning.pullCount} For an action $a \in \mathcal{A}$ and a time $t \in \mathbb{N}$, we denote by $N_{t,a}$ the number of times that action $a$ has been chosen before time $t$, that is $N_{t,a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\}$. @@ -434,6 +434,7 @@ \section{Finitely many actions} \end{lemma} \begin{proof}\leanok + \uses{def:history,lem:pullCount_basic} \end{proof} @@ -467,6 +468,7 @@ \section{Finitely many actions} \end{lemma} \begin{proof}\leanok + \uses{lem:pullCount_basic,def:pullCount} \end{proof} @@ -479,6 +481,7 @@ \section{Finitely many actions} \end{lemma} \begin{proof}\leanok + \uses{def:history,lem:pullCount_basic,def:pullCount} A hitting time of a set by an adapted process is a stopping time. \end{proof} @@ -505,6 +508,7 @@ \section{Finitely many actions} \end{lemma} \begin{proof}\leanok + \uses{lem:stepsUntil_basic,def:stepsUntil} This is perhaps hard to parse at first sight, but it follows directly from the definitions. At time $t$, the action chosen is $A_t$ and we see a reward $R_t$. That action had already been chosen $N_{t, A_t}$ times before time $t$, so the reward $R_t$ is the reward received when choosing action $A_t$ for the $(N_{t, A_t} + 1)$-th time, which is $Y_{N_{t, A_t} + 1, A_t}$ by definition. @@ -529,7 +533,6 @@ \section{Scalar rewards} \begin{definition}[Sum of rewards]\label{def:sumRewards} - \uses{def:IT.actionReward} \leanok \lean{Learning.sumRewards} Let $S_{t, a} = \sum_{s=0}^{t-1} R_s \mathbb{I}\{A_s = a\}$ be the sum of the rewards obtained by chosing action $a$ before time $t$. @@ -561,5 +564,6 @@ \section{Scalar rewards} \end{lemma} \begin{proof}\leanok + \uses{lem:rewardByCount_pullCount} \end{proof} diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index d377caf3..b304f593 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -26,7 +26,7 @@ \section{Algorithm, bandit and probability space} \begin{definition}[Bandit probability space]\label{def:Bandit.measure} - \uses{def:algorithm, def:bandit, def:trajMeasure} + \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. @@ -45,6 +45,7 @@ \section{The array model of rewards} When pulling an arm, the algorithm sees the next previously unseen reward from that arm in the array. \begin{definition}\label{def:arrayMeasure} + \uses{thm:ionescu-tulcea} % because it uses infinitePi \leanok \lean{Bandits.ArrayModel.probSpace, Bandits.ArrayModel.arrayMeasure} Let $I = [0,1]$ and let $P_U$ be the uniform distribution on $I$. We define the probability space $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$, where @@ -106,19 +107,20 @@ \subsection{Measurability} \end{remark} \begin{lemma}[Measurability]\label{lem:AM.measurable_hist} - \uses{def:AM.history} - \leanok + \uses{def:AM.history,def:arrayMeasure,def:algorithm} +\leanok \lean{Bandits.ArrayModel.measurable_hist, Bandits.ArrayModel.measurable_action, Bandits.ArrayModel.measurable_reward} $H_t$, $N_{t,A_t}$, $A_t$ and $R_t$ are measurable for all $t \in \mathbb{N}$. \end{lemma} \begin{proof}\leanok + \uses{def:algFunction,def:AM.history} \end{proof} \begin{lemma}[Congruence for the history]\label{lem:AM.hist_congr} - \uses{def:AM.history} + \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount} \leanok \lean{Bandits.ArrayModel.hist_congr} Let $\omega, \omega' \in \Omega_{\mathcal{A}}$ and $t \in \mathbb{N}$. @@ -133,13 +135,14 @@ \subsection{Measurability} \end{lemma} \begin{proof}\leanok + \uses{def:AM.history,def:algFunction,lem:pullCount_basic} \end{proof} \begin{lemma}[Congruence for the number of pulls and action]\label{lem:AM.stepsUntil_congr} - \uses{def:AM.history, def:pullCount} - \leanok + \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount} +\leanok \lean{Bandits.ArrayModel.stepsUntil_congr} Let $\omega, \omega' \in \Omega_{\mathcal{A}}$, $t, m \in \mathbb{N}$ and $a \in \mathcal{A}$. Suppose that @@ -155,12 +158,13 @@ \subsection{Measurability} \end{lemma} \begin{proof}\leanok - \uses{lem:AM.hist_congr} + \uses{def:AM.history,def:algFunction,lem:AM.hist_congr} \end{proof} \begin{definition}\label{def:AM.probSpaceSubsets} + \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount} \leanok \lean{Bandits.ArrayModel.truePast} We define the following functions on $\Omega_{\mathcal{A}}$: @@ -182,66 +186,66 @@ \subsection{Measurability} \begin{lemma}\label{lem:AM.measurable_hist_todo} - \uses{def:AM.probSpaceSubsets, def:AM.history} - \leanok + \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:AM.probSpaceSubsets} +\leanok \lean{Bandits.ArrayModel.measurable_hist_todo, Bandits.ArrayModel.measurable_hist_truePast} For all $t \in \mathbb{N}$, $H_t$ is measurable with respect to the sigma-algebra generated by $F_{1, t}$, and with respect to the sigma-algebra generated by $F_{2, a, t}$ for any arm $a \in \mathcal{A}$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.measurable_hist, lem:AM.hist_congr} + \uses{def:AM.history,lem:AM.measurable_hist,def:pullCount,lem:AM.hist_congr} \end{proof} \begin{lemma}\label{lem:AM.measurable_action_add_one_truePast} - \uses{def:AM.probSpaceSubsets, def:AM.history} + \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:AM.probSpaceSubsets} \leanok \lean{Bandits.ArrayModel.measurable_action_add_one_truePast} $A_{t+1}$ is measurable with respect to the sigma-algebra generated by $F_{2, a, t}$ for any arm $a \in \mathcal{A}$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.measurable_hist_todo} + \uses{def:AM.history,lem:AM.measurable_hist_todo,def:algFunction} \end{proof} \begin{lemma}\label{lem:AM.measurable_pullCount_add_one_truePast} - \uses{def:AM.probSpaceSubsets, def:pullCount} + \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:AM.probSpaceSubsets,def:pullCount} \leanok \lean{Bandits.ArrayModel.measurable_pullCount_add_one_truePast} $N_{t+1,a}$ is measurable with respect to the sigma-algebra generated by $F_{2, a, t}$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.measurable_hist_todo} + \uses{def:AM.history,lem:AM.measurable_hist_todo,def:algFunction} \end{proof} \begin{lemma}\label{lem:AM.measurable_stepsUntil} - \uses{def:AM.probSpaceSubsets, def:pullCount} - \leanok + \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount,def:AM.probSpaceSubsets} +\leanok \lean{Bandits.ArrayModel.measurable_stepsUntil} For $t, m \in \mathbb{N}$ and $a \in \mathcal{A}$, the indicator function $\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\} : \Omega_{\mathcal{A}} \to \{0, 1\}$ is measurable with respect to the sigma-algebra generated by $F_{2, a}^m$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.stepsUntil_congr, lem:AM.measurable_hist} + \uses{lem:AM.measurable_hist,lem:AM.stepsUntil_congr} \end{proof} \begin{lemma}\label{lem:AM.measurable_pullCount_action_add_one_hist} - \uses{def:AM.history, def:pullCount} - \leanok + \uses{def:AM.history,def:arrayMeasure,def:algorithm,def:pullCount} +\leanok \lean{Bandits.ArrayModel.measurable_pullCount_action_add_one_hist} For $t \in \mathbb{N}$, the function $N_{t+1, A_{t+1}}$ is measurable with respect to the sigma-algebra generated by $H_t$ and $A_{t+1}$. \end{lemma} \begin{proof}\leanok - \uses{lem:pullCount_basic} + \uses{def:algFunction} \end{proof} @@ -250,64 +254,66 @@ \subsection{Independence} \begin{lemma}\label{lem:AM.indepFun_fst_add_one_aux} - \uses{def:AM.probSpaceSubsets} + \uses{def:AM.probSpaceSubsets, def:arrayMeasure} \leanok \lean{Bandits.ArrayModel.indepFun_fst_add_one_aux} $\omega \mapsto \omega_{1, t+1}$ is independent of $F_{1, t}$. \end{lemma} \begin{proof}\leanok + \uses{thm:ionescu-tulcea} \end{proof} \begin{lemma}\label{lem:AM.indepFun_fst_add_one_hist} - \uses{def:AM.history, def:AM.probSpaceSubsets} + \uses{def:AM.history,def:AM.probSpaceSubsets, def:arrayMeasure,def:algorithm} \leanok \lean{Bandits.ArrayModel.indepFun_fst_add_one_hist} $\omega \mapsto \omega_{1, t+1}$ is independent of $H_t$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.measurable_hist_todo, lem:AM.indepFun_fst_add_one_aux} + \uses{lem:AM.measurable_hist_todo,lem:AM.indepFun_fst_add_one_aux} \end{proof} \begin{lemma}\label{lem:AM.indepFun_snd_apply_aux} - \uses{def:AM.probSpaceSubsets} + \uses{def:arrayMeasure,def:AM.probSpaceSubsets} \leanok \lean{Bandits.ArrayModel.indepFun_snd_apply_aux} For $a \in \mathcal{A}$ and $m \in \mathbb{N}$, $\omega \mapsto \omega_{2, m, a}$ is independent of $F_{2, a}^m$. \end{lemma} \begin{proof}\leanok + \uses{thm:ionescu-tulcea} \end{proof} \begin{lemma}\label{lem:AM.indepFun_snd_apply_pullCount_action} - \uses{def:AM.history, def:pullCount, def:AM.probSpaceSubsets} + \uses{def:arrayMeasure,def:AM.history,def:algorithm,def:pullCount,def:AM.probSpaceSubsets} \leanok \lean{Bandits.ArrayModel.indepFun_snd_apply_pullCount_action} For $a \in \mathcal{A}$, $\omega \mapsto \omega_{2, m, a}$ is independent of the indicator function $\mathbb{I}\{N_{t+1,a} = m \wedge A_{t+1} = a\}$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.measurable_stepsUntil, lem:AM.indepFun_snd_apply_aux} + \uses{lem:AM.indepFun_snd_apply_aux,lem:AM.measurable_stepsUntil} \end{proof} \begin{lemma}\label{lem:AM.indepFun_snd_hist_cond} - \uses{def:AM.history, def:pullCount} + \uses{def:arrayMeasure,def:AM.history,def:algorithm,def:pullCount} \leanok \lean{Bandits.ArrayModel.indepFun_snd_hist_cond} For $a \in \mathcal{A}$ and $t, m \in \mathbb{N}$, $\omega \mapsto \omega_{2, m, a}$ is independent of $H_t$ given that $N_{t+1,a} = m$ and $A_{t+1} = a$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.measurable_stepsUntil, lem:AM.measurable_hist_todo, lem:AM.indepFun_snd_apply_aux} + \uses{lem:AM.measurable_hist_todo,lem:AM.measurable_hist,lem:AM.indepFun_snd_apply_aux,lem:AM.measurable_stepsUntil,def:AM.probSpaceSubsets} \end{proof} @@ -316,104 +322,104 @@ \subsection{Laws} \begin{lemma}\label{lem:AM.hasLaw_action_zero} - \uses{def:AM.history, def:algFunction} - \leanok + \uses{def:arrayMeasure,def:AM.history,def:algorithm} +\leanok \lean{Bandits.ArrayModel.hasLaw_action_zero} The law of $A_0$ in the array model is $P_0$. \end{lemma} \begin{proof}\leanok + \uses{thm:ionescu-tulcea,def:algFunction,lem:AM.measurable_hist} \end{proof} \begin{lemma}\label{lem:AM.hasCondDistrib_reward_zero} - \uses{def:AM.history} + \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea} \leanok \lean{Bandits.ArrayModel.hasCondDistrib_reward_zero} In the array model, $P_{\mathcal{A}}[R_0 \mid A_0] = \nu$. \end{lemma} \begin{proof}\leanok + \uses{def:algFunction,lem:AM.measurable_hist,lem:condDistrib_ae_eq_cond} \end{proof} \begin{lemma}\label{lem:AM.hasCondDistrib_action} - \uses{def:AM.history} + \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea} \leanok \lean{Bandits.ArrayModel.hasCondDistrib_action} In the array model, $P_{\mathcal{A}}[A_{t+1} \mid H_t] = \pi_t$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.indepFun_fst_add_one_hist, def:algFunction} + \uses{def:AM.history,def:algFunction,lem:AM.measurable_hist,lem:AM.indepFun_fst_add_one_hist} \end{proof} \begin{lemma}\label{lem:AM.hasCondDistrib_reward_pullCount_action} - \uses{def:AM.history, def:pullCount} - \leanok + \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:pullCount} +\leanok \lean{Bandits.ArrayModel.hasCondDistrib_reward_pullCount_action} In the array model, $P_{\mathcal{A}}[R_{t+1} \mid N_{t+1,A_{t+1}}, A_{t+1}] = \nu$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.indepFun_snd_apply_pullCount_action} + \uses{def:AM.history,lem:AM.indepFun_snd_apply_pullCount_action,def:algFunction,lem:AM.measurable_hist,lem:pullCount_basic,lem:condDistrib_ae_eq_cond} \end{proof} \begin{lemma}\label{lem:AM.hasCondDistrib_reward_hist_action_pullCount} - \uses{def:AM.history, def:pullCount} - \leanok + \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:pullCount} +\leanok \lean{Bandits.ArrayModel.hasCondDistrib_reward_hist_action_pullCount} In the array model, $P_{\mathcal{A}}[R_{t+1} \mid H_t, A_{t+1}, N_{t+1,A_{t+1}}] = \nu$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.indepFun_snd_hist_cond, lem:AM.indepFun_snd_apply_pullCount_action} + \uses{lem:AM.indepFun_snd_apply_pullCount_action,lem:AM.indepFun_snd_hist_cond,def:algFunction,lem:AM.measurable_hist,lem:pullCount_basic} \end{proof} \begin{lemma}\label{lem:AM.condIndepFun_reward_hist} - \uses{def:AM.history} + \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,lem:AM.measurable_hist,def:pullCount} \leanok \lean{Bandits.ArrayModel.condIndepFun_reward_hist} For $t \ge 0$, $R_{t+1} \ind H_t \mid A_{t+1}, N_{t+1, A_{t+1}}$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.hasCondDistrib_reward_hist_action_pullCount} + \uses{lem:AM.measurable_hist,lem:AM.hasCondDistrib_reward_hist_action_pullCount} \end{proof} \begin{lemma}\label{lem:AM.hasCondDistrib_reward} - \uses{def:AM.history} + \uses{def:arrayMeasure,def:AM.history,def:stationaryEnv,def:environment,def:algorithm,thm:ionescu-tulcea} \leanok \lean{Bandits.ArrayModel.hasCondDistrib_reward} In the array model, $P_{\mathcal{A}}[R_{t+1} \mid H_t, A_{t+1}] = \nu$. \end{lemma} \begin{proof}\leanok - \uses{lem:AM.measurable_pullCount_action_add_one_hist, lem:AM.condIndepFun_reward_hist, - lem:AM.hasCondDistrib_reward_pullCount_action} + \uses{def:AM.history,lem:AM.measurable_pullCount_action_add_one_hist,lem:AM.hasCondDistrib_reward_pullCount_action,def:algFunction,lem:AM.measurable_hist,lem:AM.condIndepFun_reward_hist,def:pullCount} \end{proof} \begin{theorem}\label{thm:isAlgEnvSeq_arrayMeasure} - \uses{def:bandit, def:arrayMeasure, def:IsAlgEnvSeq} + \uses{def:arrayMeasure,def:AM.history,def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea} \leanok \lean{Bandits.ArrayModel.isAlgEnvSeq_arrayMeasure} The actions and rewards defined on the array model probability space $(\Omega_{\mathcal{A}}, P_{\mathcal{A}})$ form an algorithm-environment sequence for the algorithm $\mathfrak{A}$ and bandit $\nu$. \end{theorem} \begin{proof}\leanok - \uses{lem:AM.hasLaw_action_zero, lem:AM.hasCondDistrib_reward_zero, - lem:AM.hasCondDistrib_action, lem:AM.hasCondDistrib_reward} + \uses{lem:AM.hasCondDistrib_action,def:environment,lem:AM.hasCondDistrib_reward,lem:AM.measurable_hist,def:history,lem:AM.hasLaw_action_zero,lem:AM.hasCondDistrib_reward_zero} The four conditions of Definition~\ref{def:IsAlgEnvSeq} are satisfied by Lemmas~\ref{lem:AM.hasLaw_action_zero}, \ref{lem:AM.hasCondDistrib_reward_zero}, \ref{lem:AM.hasCondDistrib_action} and \ref{lem:AM.hasCondDistrib_reward}. \end{proof} @@ -429,26 +435,27 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model} \begin{lemma}\label{lem:measurable_comap_indicator_stepsUntil_eq} - \uses{def:stepsUntil} + \uses{def:history,def:stepsUntil} \leanok \lean{Learning.measurable_comap_indicator_stepsUntil_eq} The function $\mathbb{I}\{T_{n,a} = t\} : \Omega \to \{0, 1\}$ is measurable with respect to the sigma-algebra generated by $(H_{t-1}, A_t)$. \end{lemma} \begin{proof}\leanok + \uses{lem:stepsUntil_basic,lem:pullCount_basic,def:pullCount,def:IsAlgEnvSeq.filtration} \end{proof} \begin{lemma}\label{lem:condIndepFun_reward_stepsUntil_arm} - \uses{def:stepsUntil, def:IT.actionReward, def:Bandit.measure} + \uses{def:stationaryEnv,def:environment,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:stepsUntil} \leanok \lean{Bandits.condIndepFun_reward_stepsUntil_action} For $t > 0$, $R_t \ind \mathbb{I}\{T_{n, a} = t\} \mid A_t$. \end{lemma} \begin{proof}\leanok - \uses{lem:measurable_comap_indicator_stepsUntil_eq, lem:condIndepFun_reward_hist_action, lem:CondIndepFun.prod_right} + \uses{lem:condIndepFun_reward_hist_action,lem:CondIndepFun.prod_right,lem:stepsUntil_basic,lem:measurable_comap_indicator_stepsUntil_eq,def:history,def:pullCount} $\mathbb{I}\{T_{n, a} = t\}$ is measurable with respect to the sigma-algebra generated by $(H_{t-1}, A_t)$ by Lemma~\ref{lem:measurable_comap_indicator_stepsUntil_eq}. It thus suffices to show that $R_t \ind (H_{t-1}, A_t) \mid A_t$, which is implied by $R_t \ind H_{t-1} \mid A_t$ (Lemma~\ref{lem:CondIndepFun.prod_right}), which is Lemma~\ref{lem:condIndepFun_reward_hist_action}. @@ -456,7 +463,7 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model} \begin{lemma}\label{lem:reward_cond_stepsUntil} - \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:stepsUntil} \leanok \lean{Bandits.reward_cond_stepsUntil} Let $n > 0$, $t \in \mathbb{N}$ and suppose that $P(T_{n, a} = t) > 0$. @@ -464,7 +471,7 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model} \end{lemma} \begin{proof}\leanok - \uses{lem:stepsUntil_basic, lem:condIndepFun_reward_stepsUntil_arm, lem:condDistrib_reward_stationaryEnv} + \uses{def:environment,lem:stepsUntil_basic,lem:condIndepFun_reward_stepsUntil_arm,def:pullCount,lem:condDistrib_ae_eq_cond,lem:condDistrib_reward_stationaryEnv} First, if $T_{n, a} = t$, then $A_t = a$ (Lemma~\ref{lem:stepsUntil_basic}), such that $\mathcal{L}(R_t \mid T_{n, a} = t) = \mathcal{L}(R_t \mid T_{n, a} = t, A_t = a)$. Then, using first the independence from Lemma~\ref{lem:condIndepFun_reward_stepsUntil_arm} and then the conditional distribution from Lemma~\ref{lem:condDistrib_reward_stationaryEnv}, we have @@ -490,14 +497,14 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model} \begin{lemma}\label{lem:condDistrib_rewardByCount_stepsUntil} - \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure} - \leanok + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:rewardByCount,def:stepsUntil} +\leanok \lean{Bandits.condDistrib_rewardByCount_stepsUntil} For $n > 0$ and $t \in \mathbb{N}$, $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \nu(a)$ (in which the measure on the r.h.s. is seen as a constant kernel). \end{lemma} \begin{proof}\leanok - \uses{lem:condDistrib_ae_eq_cond, lem:reward_cond_stepsUntil} + \uses{def:environment,lem:reward_cond_stepsUntil,def:pullCount,lem:condDistrib_ae_eq_cond} It suffices to show that for all $t \in \mathbb{N} \cup \{\infty\}$ such that $\mathbb{P}(T_{n, a} = t) > 0$, the law of $Y_{n,a}$ conditioned on $T_{n,a} = t$ is $\nu(a)$. If $t < \infty$, then $\mathcal{L}(Y_{n, a} \mid T_{n, a} = t) = \mathcal{L}(R_t \mid T_{n, a} = t) = \nu(a)$ by Lemma~\ref{lem:reward_cond_stepsUntil}. @@ -507,14 +514,14 @@ \section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model} \begin{lemma}\label{lem:hasLaw_rewardByCount} - \uses{def:rewardByCount} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:rewardByCount} \leanok \lean{Bandits.hasLaw_rewardByCount} For $n > 0$ and $a \in \mathcal{A}$, $\mathcal{L}(Y_{n,a}) = \nu(a)$. \end{lemma} \begin{proof}\leanok - \uses{lem:condDistrib_rewardByCount_stepsUntil} + \uses{def:environment,lem:condDistrib_rewardByCount_stepsUntil,def:stepsUntil,def:pullCount} The law of $Y_{n,a}$ is given by $\mathcal{L}(Y_{n, a}) = \mathcal{L}(Y_{n, a} \mid T_{n, a}) \circ \mathcal{L}(T_{n, a})$. By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $\mathcal{L}(Y_{n, a} \mid T_{n, a}) = \nu(a)$, a constant kernel. Thus the composition is just $\nu(a)$. @@ -644,7 +651,7 @@ \section{Regret and other bandit quantities} \begin{definition}[Regret]\label{def:regret} - \uses{def:armMean, def:IT.actionReward} + \uses{def:armMean} \leanok \lean{Bandits.regret} The regret $R_T$ of a sequence of arms $A_0, \ldots, A_{T-1}$ after $T$ pulls is the difference between the cumulative reward of always playing the best arm and the cumulative reward of the sequence: diff --git a/blueprint/src/chapters/concentration.tex b/blueprint/src/chapters/concentration.tex index c8fcee70..0e5dd54b 100644 --- a/blueprint/src/chapters/concentration.tex +++ b/blueprint/src/chapters/concentration.tex @@ -79,7 +79,7 @@ \section{Sub-Gaussian random variables} \end{lemma} \begin{proof}\leanok - \uses{lem:subGaussian_add_of_indepFun, thm:hoeffding} + \uses{lem:subGaussian_add_of_indepFun, lem:hoeffding_one} \end{proof} @@ -90,20 +90,20 @@ \section{Concentration of the sums of rewards in bandit models} \begin{lemma}\label{lem:AM.identDistrib_pullCount_prod_sumRewards} - \uses{def:rewardByCount, def:sumRewards, def:pullCount, def:AM.history} + \uses{def:arrayMeasure,def:AM.history,def:algorithm,def:sumRewards,def:pullCount} \leanok \lean{Bandits.ArrayModel.identDistrib_pullCount_prod_sumRewards} In the array model, for $t \in \mathbb{N}$, the random variable $(N_{t,a}, S_{t, a})_{a \in \mathcal{A}}$ has the same distribution as $(N_{t,a}, \sum_{s=0}^{N_{t,a}-1} \omega_{2, s, a})_{a \in \mathcal{A}}$. \end{lemma} \begin{proof}\leanok - \uses{def:AM.history, lem:AM.measurable_hist, lem:sum_rewardByCount} + \uses{def:AM.history,lem:stepsUntil_basic,thm:ionescu-tulcea,def:algFunction,lem:AM.measurable_hist,def:rewardByCount,lem:pullCount_basic,def:stepsUntil,lem:sum_rewardByCount} \end{proof} \begin{lemma}\label{lem:AM.identDistrib_sum_range_snd} - \uses{def:AM.history} + \uses{def:arrayMeasure,thm:ionescu-tulcea} \leanok \lean{Bandits.ArrayModel.identDistrib_sum_range_snd} In the array model, for $k \in \mathbb{N}$, the random variable $\sum_{s=0}^{k-1} \omega_{2, s, a}$ has the same distribution as a sum of $k$ i.i.d. random variables with law $\nu(a)$. @@ -115,7 +115,7 @@ \section{Concentration of the sums of rewards in bandit models} \begin{lemma}\label{lem:prob_pullCount_prod_sumRewards_mem_le} - \uses{def:sumRewards, def:pullCount, def:AM.history} + \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:sumRewards,def:pullCount,def:stationaryEnv,def:IsAlgEnvSeq} \leanok \lean{Bandits.ArrayModel.prob_pullCount_prod_sumRewards_mem_le, Bandits.prob_pullCount_prod_sumRewards_mem_le} In the array model, for $t \in \mathbb{N}$, $a \in \mathcal{A}$, and a measurable set $B \subseteq \mathbb{N} \times \mathbb{R}$, @@ -128,13 +128,13 @@ \section{Concentration of the sums of rewards in bandit models} \end{lemma} \begin{proof}\leanok - \uses{lem:AM.identDistrib_pullCount_prod_sumRewards, lem:AM.identDistrib_sum_range_snd, thm:isAlgEnvSeq_unique, thm:isAlgEnvSeq_arrayMeasure} + \uses{lem:AM.identDistrib_sum_range_snd,lem:AM.identDistrib_pullCount_prod_sumRewards,lem:AM.measurable_hist,lem:pullCount_basic,def:arrayMeasure,def:AM.history,def:environment,thm:isAlgEnvSeq_arrayMeasure,lem:AM.measurable_hist,thm:isAlgEnvSeq_unique} \end{proof} \begin{lemma}\label{lem:prob_sumRewards_le_sumRewards_le} - \uses{def:sumRewards, def:pullCount, def:AM.history} + \uses{def:arrayMeasure,def:AM.history,def:algorithm,thm:ionescu-tulcea,def:sumRewards,def:pullCount,def:stationaryEnv,def:IsAlgEnvSeq} \leanok \lean{Bandits.ArrayModel.prob_sumRewards_le_sumRewards_le, Bandits.probReal_sumRewards_le_sumRewards_le} In the array model, @@ -147,7 +147,7 @@ \section{Concentration of the sums of rewards in bandit models} \end{lemma} \begin{proof}\leanok - \uses{lem:AM.identDistrib_pullCount_prod_sumRewards, lem:AM.identDistrib_sum_range_snd, thm:isAlgEnvSeq_unique,thm:isAlgEnvSeq_arrayMeasure} + \uses{lem:AM.identDistrib_pullCount_prod_sumRewards,lem:AM.measurable_hist,lem:pullCount_basic,def:arrayMeasure,def:AM.history,def:environment,thm:isAlgEnvSeq_arrayMeasure,lem:AM.measurable_hist,thm:isAlgEnvSeq_unique} \end{proof} @@ -158,6 +158,7 @@ \subsection{Sub-Gaussian rewards} TODO: extend this to sub-Gaussian with constant other than 1. \begin{lemma}\label{lem:probReal_sum_le_sum_streamMeasure} + \uses{thm:ionescu-tulcea,def:subGaussian,def:gap} \leanok \lean{Bandits.probReal_sum_le_sum_streamMeasure} Let $\nu(a)$ be a 1-sub-Gaussian distribution on $\mathbb{R}$ for each arm $a \in \mathcal{A}$. @@ -174,6 +175,7 @@ \subsection{Sub-Gaussian rewards} \begin{lemma}\label{lem:prob_sum_le_sqrt_log} + \uses{thm:ionescu-tulcea,def:subGaussian} \leanok \lean{Bandits.prob_sum_le_sqrt_log, Bandits.prob_sum_ge_sqrt_log} Let $\nu(a)$ be a 1-sub-Gaussian distribution on $\mathbb{R}$ for each arm $a \in \mathcal{A}$. diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex index e0c524c1..f3f2f096 100644 --- a/blueprint/src/chapters/etc.tex +++ b/blueprint/src/chapters/etc.tex @@ -7,6 +7,7 @@ \section{Explore-Then-Commit} Note: we will describe the algorithm by writing $A_t = ...$, but our formal bandit model needs a policy $\pi_t$ that gives the distribution of the arm to pull. What me mean is that $\pi_t$ is a Dirac distribution at that arm. \begin{definition}[Explore-Then-Commit algorithm]\label{def:etcAlgorithm} + \uses{def:detAlgorithm,def:algorithm} \leanok \lean{Bandits.ETC.nextArm, Bandits.etcAlgorithm} The Explore-Then-Commit (ETC) algorithm with parameter $m \in \mathbb{N}$ is defined as follows: @@ -19,7 +20,7 @@ \section{Explore-Then-Commit} \begin{lemma}\label{lem:pullCount_etcAlgorithm} - \uses{def:etcAlgorithm, def:pullCount} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:pullCount,def:etcAlgorithm} \leanok \lean{Bandits.ETC.pullCount_of_ge} For the Explore-Then-Commit algorithm with parameter $m$, for any arm $a \in [K]$ and any time $t \ge Km$, we have @@ -31,24 +32,26 @@ \section{Explore-Then-Commit} \end{lemma} \begin{proof}\leanok + \uses{def:environment,def:detAlgorithm,def:algorithm,def:history,lem:pullCount_basic,def:etcAlgorithm} \end{proof} \begin{lemma}\label{lem:sumRewards_bestArm_le_of_arm_mul_eq} - \uses{def:etcAlgorithm, def:sumRewards} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:sumRewards,def:etcAlgorithm} \leanok \lean{Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq} If $\hat{A}_m^* = a$, then we have $S_{Km, a^*} \le S_{Km, a}$. \end{lemma} \begin{proof}\leanok + \uses{def:environment,def:detAlgorithm,def:algorithm,def:history,def:pullCount,def:empMean,def:etcAlgorithm} \end{proof} \begin{lemma}\label{lem:prob_etc_error_le_exp} - \uses{def:etcAlgorithm} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:subGaussian,def:gap,def:etcAlgorithm} \leanok \lean{Bandits.ETC.prob_arm_mul_eq_le} Suppose that $\nu(a)$ is 1-sub-Gaussian for all arms $a \in [K]$. @@ -56,7 +59,7 @@ \section{Explore-Then-Commit} \end{lemma} \begin{proof}\leanok - \uses{lem:prob_sumRewards_le_sumRewards_le, lem:probReal_sum_le_sum_streamMeasure, lem:sumRewards_bestArm_le_of_arm_mul_eq} + \uses{def:environment,lem:probReal_sum_le_sum_streamMeasure,lem:prob_sumRewards_le_sumRewards_le,def:detAlgorithm,def:algorithm,thm:ionescu-tulcea,def:sumRewards,def:history,lem:sumRewards_bestArm_le_of_arm_mul_eq,def:pullCount,def:etcAlgorithm} By Lemma~\ref{lem:sumRewards_bestArm_le_of_arm_mul_eq}, \begin{align*} \mathbb{P}(\hat{A}_m^* = a) @@ -75,7 +78,7 @@ \section{Explore-Then-Commit} \begin{theorem}\label{thm:regret_etc_le} - \uses{def:etcAlgorithm, def:regret} + \uses{def:stationaryEnv,def:regret,def:IsAlgEnvSeq,def:subGaussian,def:gap,def:etcAlgorithm} \leanok \lean{Bandits.ETC.regret_le} Suppose that $\nu(a)$ is 1-sub-Gaussian for all arms $a \in [K]$. @@ -88,7 +91,7 @@ \section{Explore-Then-Commit} \end{theorem} \begin{proof}\leanok - \uses{lem:regret_eq_sum_pullCount_mul_gap, lem:pullCount_etcAlgorithm, lem:prob_etc_error_le_exp} + \uses{lem:pullCount_etcAlgorithm,def:environment,def:algorithm,lem:regret_eq_sum_pullCount_mul_gap,lem:prob_etc_error_le_exp,lem:pullCount_basic,def:pullCount} By Lemma~\ref{lem:regret_eq_sum_pullCount_mul_gap}, we have $\mathbb{E}[R_T] = \sum_{a=1}^K \mathbb{E}\left[N_{T,a}\right] \Delta_a$~. It thus suffices to bound $\mathbb{E}[N_{T,a}]$ for each arm $a$ with $\Delta_a > 0$. It suffices to prove that diff --git a/blueprint/src/chapters/ucb.tex b/blueprint/src/chapters/ucb.tex index 6029a226..343d830d 100644 --- a/blueprint/src/chapters/ucb.tex +++ b/blueprint/src/chapters/ucb.tex @@ -1,7 +1,7 @@ \section{UCB} \begin{definition}[UCB algorithm]\label{def:ucbAlgorithm} - \uses{def:IT.actionReward, def:pullCount, def:empMean} + \uses{def:detAlgorithm,def:algorithm} \leanok \lean{Bandits.UCB.nextArm, Bandits.ucbAlgorithm} The UCB algorithm with parameter $c \in \mathbb{R}_+$ is defined as follows: @@ -15,7 +15,7 @@ \section{UCB} \begin{lemma}\label{lem:ucbIndex_le_ucbIndex_arm} - \uses{def:ucbAlgorithm} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm,def:pullCount,def:empMean} \leanok \lean{Bandits.UCB.ucbIndex_le_ucbIndex_arm} For the UCB algorithm, for all time $t \ge K$ and arm $a \in [K]$, we have @@ -27,12 +27,13 @@ \section{UCB} \end{lemma} \begin{proof}\leanok + \uses{def:environment,def:detAlgorithm,def:algorithm,def:sumRewards,def:ucbAlgorithm,def:history} By definition of the algorithm. \end{proof} \begin{lemma}\label{lem:gap_arm_le_two_mul_ucbWidth} - \uses{def:ucbAlgorithm} + \uses{def:pullCount,def:gap,def:empMean,def:pullCount,def:gap,def:empMean} \leanok \lean{Bandits.UCB.gap_arm_le_two_mul_ucbWidth, Bandits.UCB.pullCount_arm_le} Suppose that we have the 3 following conditions: @@ -63,7 +64,7 @@ \section{UCB} \begin{lemma}\label{lem:prob_ucbIndex_le} - \uses{def:empMean, def:pullCount} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:subGaussian,def:ucbAlgorithm,def:pullCount,def:empMean} \leanok \lean{Bandits.UCB.prob_ucbIndex_le, Bandits.UCB.prob_ucbIndex_ge} Suppose that $\nu(a)$ is 1-sub-Gaussian for all arms $a \in [K]$. @@ -83,13 +84,13 @@ \section{UCB} \end{lemma} \begin{proof}\leanok - \uses{lem:prob_pullCount_prod_sumRewards_mem_le, lem:prob_sum_le_sqrt_log, lem:pullCount_basic} + \uses{lem:prob_sum_le_sqrt_log,thm:ionescu-tulcea,lem:prob_pullCount_prod_sumRewards_mem_le} \end{proof} \begin{lemma}\label{lem:pullCount_le_add_three} - \uses{def:pullCount, def:empMean} + \uses{def:pullCount,def:empMean,def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm} \leanok \lean{Bandits.UCB.pullCount_le_add_three, Bandits.UCB.pullCount_le_add_three_ae} For $C$ a natural number, for any time $n \in \mathbb{N}$ and any arm $a \in [K]$, we have @@ -112,25 +113,26 @@ \section{UCB} \end{lemma} \begin{proof}\leanok + \uses{def:environment,def:detAlgorithm,def:algorithm,def:ucbAlgorithm,def:history,lem:pullCount_basic} \end{proof} \begin{lemma}\label{lem:some_sum_eq_zero} - \uses{def:pullCount, def:empMean, def:ucbAlgorithm} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:ucbAlgorithm,def:pullCount,def:gap,def:empMean} \leanok \lean{Bandits.UCB.some_sum_eq_zero} For the UCB algorithm with parameter $c \ge 0$, for any time $n \in \mathbb{N}$ and any arm $a \in [K]$ with positive gap, the first sum in Lemma~\ref{lem:pullCount_le_add_three} is equal to zero for positive $C$ such that $C \ge \frac{4 c \log(n + 1)}{\Delta_a^2}$. \end{lemma} \begin{proof}\leanok - \uses{lem:gap_arm_le_two_mul_ucbWidth, lem:ucbIndex_le_ucbIndex_arm} + \uses{def:environment,def:detAlgorithm,def:algorithm,def:ucbAlgorithm,lem:ucbIndex_le_ucbIndex_arm,def:history,lem:pullCount_basic,lem:gap_arm_le_two_mul_ucbWidth} \end{proof} \begin{lemma}\label{lem:expectation_pullCount_le} - \uses{def:ucbAlgorithm, def:pullCount, def:empMean} + \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:subGaussian,def:ucbAlgorithm,def:pullCount,def:gap} \leanok \lean{Bandits.UCB.expectation_pullCount_le} Suppose that $\nu(a)$ is 1-sub-Gaussian for all arms $a \in [K]$. @@ -143,13 +145,13 @@ \section{UCB} \end{lemma} \begin{proof}\leanok - \uses{lem:pullCount_le_add_three, lem:some_sum_eq_zero, lem:prob_ucbIndex_le} + \uses{def:environment,def:algorithm,def:sumRewards,lem:some_sum_eq_zero,lem:prob_ucbIndex_le,lem:pullCount_basic,def:empMean,lem:pullCount_le_add_three} \end{proof} \begin{lemma}\label{lem:ucb_regret_le} - \uses{def:ucbAlgorithm, def:regret} + \uses{def:stationaryEnv,def:regret,def:IsAlgEnvSeq,def:subGaussian,def:ucbAlgorithm,def:gap} \leanok \lean{Bandits.UCB.regret_le} Suppose that $\nu(a)$ is 1-sub-Gaussian for all arms $a \in [K]$. @@ -162,7 +164,7 @@ \section{UCB} \end{lemma} \begin{proof}\leanok - \uses{lem:expectation_pullCount_le, lem:regret_eq_sum_pullCount_mul_gap} + \uses{def:environment,def:algorithm,lem:regret_eq_sum_pullCount_mul_gap,lem:pullCount_basic,lem:expectation_pullCount_le,def:pullCount} \end{proof}