From 6f73bbaaaa1b9ccd4766bc652fbcb8be836e23b2 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 4 Sep 2025 10:51:29 +0200 Subject: [PATCH 1/4] blueprint update --- blueprint/lean_decls | 1 + blueprint/src/chapters/bandit.tex | 83 +++++++++++++++++++++---------- blueprint/src/macros/common.tex | 7 +-- 3 files changed, 62 insertions(+), 29 deletions(-) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 10af5c83..f95781ca 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,3 +1,4 @@ +Bandits.Algorithm Bandits.Bandit.measure Bandits.arm Bandits.reward diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 7c5fe7bd..85875164 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -1,25 +1,44 @@ \chapter{Stochastic multi-armed bandits} -\section{Bandit model and probability space} +\section{Algorithm, bandit and probability space} -TODO: refactor the following to reflect the change in the code. - -\begin{definition}[Bandit]\label{def:bandit} +\begin{definition}[Algorithm]\label{def:algorithm} \leanok -The interaction of an algorithm with a stochastic bandit with arms in $\mathcal{A}$ (a measurable space) and real rewards is described by the following data: + \lean{Bandits.Algorithm} +A sequential, stochastic algorithm with actions in a measurable space $\mathcal{A}$ and observations in a measurable space $\mathcal{R}$ is described by the following data: \begin{itemize} - \item $\nu : \mathcal{A} \rightsquigarrow \mathbb{R}$, a Markov kernel, conditional distribution of the rewards given the arm pulled, - \item for all $t \in \mathbb{N}$, a policy $\pi_t : (\mathcal{A} \times \mathbb{R})^{t+1} \rightsquigarrow \mathcal{A}$, a Markov kernel which gives the distribution of the arm to pull at time $t+1$ given the history of previous pulls and rewards, + \item for all $t \in \mathbb{N}$, a policy $\pi_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow \mathcal{A}$, a Markov kernel which gives the distribution of the arm to pull at time $t+1$ given the history of previous pulls and observations, \item $P_0 \in \mathcal{P}(\mathcal{A})$, a probability measure that gives the distribution of the first arm to pull. \end{itemize} \end{definition} +The first arm pulled by the algorithm is sampled from $P_0$, the arm pulled at time $1$ is sampled from $\pi_0(H_0)$, where $H_0 \in \mathcal{A} \times \mathcal{R}$ is the data of the first arm pulled and the first observation received, and so on. + + +\begin{definition}[Bandit]\label{def:bandit} + \mathlibok +A stochastic bandit is simply a reward distribution for each arm: a Markov kernel $\nu : \mathcal{A} \rightsquigarrow \mathbb{R}$, conditional distribution of the rewards given the arm pulled. +\end{definition} + + +Note: we don't have a Lean definition for a bandit, since it is just a Markov kernel. + +An algorithm can interact with a bandit to produce a sequence of arms and rewards: after a time $t$, the history $H_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$ contains the arms pulled and rewards received up to that time, +\begin{itemize} + \item the algorithm chooses an arm $A_{t+1}$ sampled according to its policy $\pi_t(H_t)$, + \item the bandit generates a reward $X_{t+1}$ according to the distribution $\nu(A_{t+1})$, + \item the history is updated to $H_{t+1} = ((A_0, X_0), \ldots, (A_{t+1}, X_{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:bandit} + \uses{def:algorithm, def:bandit} \leanok \lean{Bandits.Bandit.measure} -By an application of the Ionescu-Tulcea theorem, a bandit $\mathcal{B} = (\nu, \pi, P_0)$ defines a probability distribution on the space $\Omega := (\mathcal{A} \times \mathbb{R})^{\mathbb{N}}$, the space of infinite sequences of arms and rewards. +By an application of the Ionescu-Tulcea theorem, an algorithm $(\pi, P_0)$ and bandit $\nu$ together defines a probability distribution on the space $\Omega := (\mathcal{A} \times \mathbb{R})^{\mathbb{N}}$, the space of infinite sequences of arms and rewards. We denote that distribution by $\mathbb{P}$. TODO: explain how the probability distribution is constructed. \end{definition} @@ -35,6 +54,18 @@ \section{Bandit model and probability space} \end{definition} +\begin{remark}[Building vs analyzing algorithms] +When we describe an algorithm, we give the data of the policies $\pi_t$, which are functions of the partial history up to time $t$, in $(\mathcal{A} \times \mathcal{R})^{t+1}$. +That means that any tool used to define a policy must be a function defined on $(\mathcal{A} \times \mathcal{R})^{t+1}$. +For example a definition of the empirical mean of an arm must be a function $t : \mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{t+1} \to \mathbb{R}$. + +When we analyze an algorithm, we work on the other hand on the bandit probability space $(\Omega, \mathbb{P})$, in which $\Omega = (\mathcal{A} \times \mathcal{R})^{\mathbb{N}}$ is the full history, which describes the whole sequence of arms and rewards. +As a stochastic process, the empirical mean of an arm is a function $\mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{\mathbb{N}} \to \mathbb{R}$. + +Thus there are two very distinct types of objects: those defined on the partial history, which are used to build algorithms, and those defined on the full history, which are used to analyze algorithms. +\end{remark} + + \begin{lemma}\label{lem:condDistrib_reward} \uses{def:Bandit.measure,def:armAndReward} \leanok @@ -138,7 +169,7 @@ \section{Alternative model} An alternative way to talk about that process is to imagine that there is a stream of rewards from each arm, and that the algorithm sees the first, then second, etc. reward from the arms at it pulls them. We introduce definitions to talk about the $n^{th}$ reward of an arm, and the time at which that reward is pulled. -\begin{definition}\label{def:timeOfPull} +\begin{definition}\label{def:stepsUntil} \uses{def:pullCount} \leanok \lean{Bandits.stepsUntil} @@ -147,8 +178,8 @@ \section{Alternative model} \end{definition} -\begin{definition}\label{def:altReward} - \uses{def:timeOfPull} +\begin{definition}\label{def:rewardByCount} + \uses{def:stepsUntil} \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. @@ -157,8 +188,8 @@ \section{Alternative model} TODO: that definition requires changing the probability space to $\Omega \times \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$. -\begin{lemma}\label{lem:iid_altReward} - \uses{def:altReward} +\begin{lemma}\label{lem:iid_rewardByCount} + \uses{def:rewardByCount} The rewards $(Y_{n,a})_{n \in \mathbb{N}}$ are independent and identically distributed random variables, with distribution $\nu(a)$. \end{lemma} @@ -167,8 +198,8 @@ \section{Alternative model} \end{proof} -\begin{lemma}\label{lem:independent_altReward} - \uses{def:altReward} +\begin{lemma}\label{lem:independent_rewardByCount} + \uses{def:rewardByCount} 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} @@ -177,8 +208,8 @@ \section{Alternative model} \end{proof} -\begin{lemma}\label{lem:timeOfPull_pullCount_le} - \uses{def:timeOfPull,def:pullCount} +\begin{lemma}\label{lem:stepsUntil_pullCount_le} + \uses{def:stepsUntil,def:pullCount} \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}$. @@ -189,8 +220,8 @@ \section{Alternative model} \end{proof} -\begin{lemma}\label{lem:timeOfPull_pullCount_eq} - \uses{def:timeOfPull,def:pullCount} +\begin{lemma}\label{lem:stepsUntil_pullCount_eq} + \uses{def:stepsUntil,def:pullCount} \leanok \lean{Bandits.stepsUntil_pullCount_eq} $T_{N_{t+1, A_t}, A_t} = t$ for all $t \in \mathbb{N}$. @@ -201,22 +232,22 @@ \section{Alternative model} \end{proof} -\begin{lemma}\label{lem:altReward_pullCount} - \uses{def:altReward,def:pullCount} +\begin{lemma}\label{lem:rewardByCount_pullCount} + \uses{def:rewardByCount,def:pullCount} \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}\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$. + \uses{lem:stepsUntil_pullCount_eq} +By Lemma~\ref{lem:stepsUntil_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$. \end{proof} -\begin{lemma}\label{lem:sum_altReward} - \uses{def:altReward,def:pullCount} +\begin{lemma}\label{lem:sum_rewardByCount} + \uses{def:rewardByCount,def:pullCount} \leanok \lean{Bandits.sum_rewardByCount_eq_sum_reward} \begin{align*} diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex index 83d71e14..e579e1ff 100644 --- a/blueprint/src/macros/common.tex +++ b/blueprint/src/macros/common.tex @@ -4,15 +4,16 @@ % The theorem-like environments defined below are those that appear by default % in the dependency graph. See the README of leanblueprint if you need help to -% customize this. +% customize this. % The configuration below use the theorem counter for all those environments % (this is what the [theorem] arguments mean) and never resets it. % If you want for instance to number them within chapters then you can add % [chapter] at the end of the next line. -\newtheorem{theorem}{Theorem} +\newtheorem{theorem}{Theorem}[chapter] \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} -\newtheorem{definition}[theorem]{Definition} \ No newline at end of file +\newtheorem{definition}[theorem]{Definition} +\newtheorem{remark}[theorem]{Remark} From 6dfd3fcdc866d26dc4c4dc8e25e91bec9af536bc Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 4 Sep 2025 11:00:42 +0200 Subject: [PATCH 2/4] move a section --- blueprint/src/chapters/bandit.tex | 126 +++++++++++++++--------------- 1 file changed, 64 insertions(+), 62 deletions(-) diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 85875164..2275f9b1 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -100,68 +100,6 @@ \section{Algorithm, bandit and probability space} \end{proof} -\section{Regret and other bandit quantities} - -\begin{definition}\label{def:armMean} - \uses{def:bandit} - \leanok % no actual Lean def, but we don't need one -For an arm $a \in \mathcal{A}$, we denote by $\mu_a$ the mean of the rewards for that arm, that is $\mu_a = \nu(a)[X]$. -We denote by $\mu^*$ the mean of the best arm, that is $\mu^* = \max_{a \in \mathcal{A}} \mu_a$. -\end{definition} - - -\begin{definition}[Regret]\label{def:regret} - \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: -\begin{align*} - R_T = T \mu^* - \sum_{t=0}^{T-1} \mu_{A_t} \: . -\end{align*} -\end{definition} - - -\begin{definition}\label{def:gap} - \uses{def:armMean} - \leanok - \lean{Bandits.gap} -For an arm $a \in \mathcal{A}$, its gap is defined as the difference between the mean of the best arm and the mean of that arm: $\Delta_a = \mu^* - \mu_a$. -\end{definition} - - -\begin{definition}\label{def:pullCount} - \uses{def:bandit} - \leanok - \lean{Bandits.pullCount} -For an arm $a \in \mathcal{A}$ and a time $t \in \mathbb{N}$, we denote by $N_{t,a}$ the number of times that arm $a$ has been pulled before time $t$, that is $N_{t,a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\}$. -\end{definition} - - -\begin{lemma}\label{lem:regret_eq_sum_pullCount_mul_gap} - \uses{def:regret,def:gap,def:pullCount} - \leanok - \lean{Bandits.regret_eq_sum_pullCount_mul_gap} -For $\mathcal{A}$ finite, the regret $R_T$ can be expressed as a sum over the arms and their gaps: -\begin{align*} - R_T = \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a \: . -\end{align*} -\end{lemma} - -\begin{proof} - \leanok -\begin{align*} - R_T = T \mu^* - \sum_{t=0}^{T-1} \mu_{A_t} - &= T \mu^* - \sum_{a \in \mathcal{A}} \sum_{t=0}^{T-1} \mathbb{I}\{A_t = a\} \mu_a - \\ - &= T \mu^* - \sum_{a \in \mathcal{A}} N_{T,a} \mu_a - \\ - &= \sum_{a \in \mathcal{A}} N_{T,a} \mu^* - \sum_{a \in \mathcal{A}} N_{T,a} \mu_a - \\ - &= \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a - \: . -\end{align*} -\end{proof} - \section{Alternative model} @@ -259,3 +197,67 @@ \section{Alternative model} \begin{proof}\leanok \end{proof} + + + +\section{Regret and other bandit quantities} + +\begin{definition}\label{def:armMean} + \uses{def:bandit} + \leanok % no actual Lean def, but we don't need one +For an arm $a \in \mathcal{A}$, we denote by $\mu_a$ the mean of the rewards for that arm, that is $\mu_a = \nu(a)[X]$. +We denote by $\mu^*$ the mean of the best arm, that is $\mu^* = \max_{a \in \mathcal{A}} \mu_a$. +\end{definition} + + +\begin{definition}[Regret]\label{def:regret} + \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: +\begin{align*} + R_T = T \mu^* - \sum_{t=0}^{T-1} \mu_{A_t} \: . +\end{align*} +\end{definition} + + +\begin{definition}\label{def:gap} + \uses{def:armMean} + \leanok + \lean{Bandits.gap} +For an arm $a \in \mathcal{A}$, its gap is defined as the difference between the mean of the best arm and the mean of that arm: $\Delta_a = \mu^* - \mu_a$. +\end{definition} + + +\begin{definition}\label{def:pullCount} + \uses{def:bandit} + \leanok + \lean{Bandits.pullCount} +For an arm $a \in \mathcal{A}$ and a time $t \in \mathbb{N}$, we denote by $N_{t,a}$ the number of times that arm $a$ has been pulled before time $t$, that is $N_{t,a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\}$. +\end{definition} + + +\begin{lemma}\label{lem:regret_eq_sum_pullCount_mul_gap} + \uses{def:regret,def:gap,def:pullCount} + \leanok + \lean{Bandits.regret_eq_sum_pullCount_mul_gap} +For $\mathcal{A}$ finite, the regret $R_T$ can be expressed as a sum over the arms and their gaps: +\begin{align*} + R_T = \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a \: . +\end{align*} +\end{lemma} + +\begin{proof} + \leanok +\begin{align*} + R_T = T \mu^* - \sum_{t=0}^{T-1} \mu_{A_t} + &= T \mu^* - \sum_{a \in \mathcal{A}} \sum_{t=0}^{T-1} \mathbb{I}\{A_t = a\} \mu_a + \\ + &= T \mu^* - \sum_{a \in \mathcal{A}} N_{T,a} \mu_a + \\ + &= \sum_{a \in \mathcal{A}} N_{T,a} \mu^* - \sum_{a \in \mathcal{A}} N_{T,a} \mu_a + \\ + &= \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a + \: . +\end{align*} +\end{proof} From 6c37962f1b785960a5c0f30f9e48f0adb33bda65 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 4 Sep 2025 11:12:47 +0200 Subject: [PATCH 3/4] add concentration results --- blueprint/lean_decls | 10 +++--- blueprint/src/chapters/concentration.tex | 39 ++++++++++++++++++++++-- blueprint/src/chapters/etc.tex | 4 +-- 3 files changed, 45 insertions(+), 8 deletions(-) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index f95781ca..fc9eaeeb 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -5,17 +5,19 @@ Bandits.reward Bandits.hist Bandits.condDistrib_reward Bandits.condDistrib_arm -Bandits.regret -Bandits.gap -Bandits.pullCount -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 +Bandits.regret +Bandits.gap +Bandits.pullCount +Bandits.regret_eq_sum_pullCount_mul_gap ProbabilityTheory.HasSubgaussianMGF +ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun +ProbabilityTheory.HasSubgaussianMGF.measure_ge_le ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun Bandits.etcNextArm Bandits.etcAlgorithm \ No newline at end of file diff --git a/blueprint/src/chapters/concentration.tex b/blueprint/src/chapters/concentration.tex index 88fc1f0a..4e59cfef 100644 --- a/blueprint/src/chapters/concentration.tex +++ b/blueprint/src/chapters/concentration.tex @@ -3,16 +3,50 @@ \chapter{Concentration inequalities} \begin{definition}[Sub-Gaussian]\label{def:subGaussian} \mathlibok \lean{ProbabilityTheory.HasSubgaussianMGF} -TODO +A real valued random variable $X$ is $\sigma^2$-sub-Gaussian if for any $\lambda \in \mathbb{R}$, +\begin{align*} + \mathbb{E}\left[e^{\lambda X}\right] + &\le e^{\frac{\lambda^2 \sigma^2}{2}} + \: . +\end{align*} \end{definition} +\begin{lemma}\label{lem:subGaussian_add_of_indepFun} + \uses{def:subGaussian} + \mathlibok + \lean{ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun} +If $X$ is $\sigma_1^2$-sub-Gaussian and $Y$ is $\sigma_2^2$-sub-Gaussian, and $X$ and $Y$ are independent, then $X + Y$ is $(\sigma_1^2 + \sigma_2^2)$-sub-Gaussian. +\end{lemma} + +\begin{proof}\leanok + +\end{proof} + + +\begin{lemma}\label{lem:hoeffding_one} + \uses{def:subGaussian} + \mathlibok + \lean{ProbabilityTheory.HasSubgaussianMGF.measure_ge_le} +For $X$ a $\sigma^2$-sub-Gaussian random variable, for any $t \ge 0$, +\begin{align*} + \mathbb{P}(X \ge t) + &\le \exp\left(- \frac{t^2}{2 \sigma^2}\right) + \: . +\end{align*} +\end{lemma} + +\begin{proof}\leanok + +\end{proof} + + \begin{theorem}\label{thm:hoeffding} \uses{def:subGaussian} \mathlibok \lean{ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun} Let $X_1, \ldots, X_n$ be independent random variables such that $X_i$ is $\sigma_i^2$-sub-Gaussian for $i \in [n]$. -Then for any $t \ge 0$, we have +Then for any $t \ge 0$, \begin{align*} \mathbb{P}\left(\sum_{i=1}^n X_i \ge t\right) &\le \exp\left(- \frac{t^2}{2 \sum_{i=1}^n \sigma_i^2}\right) @@ -21,5 +55,6 @@ \chapter{Concentration inequalities} \end{theorem} \begin{proof}\leanok + \uses{lem:subGaussian_add_of_indepFun, lem:hoeffding_one} \end{proof} diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex index ddc6edec..113bf6ed 100644 --- a/blueprint/src/chapters/etc.tex +++ b/blueprint/src/chapters/etc.tex @@ -40,7 +40,7 @@ \section{Explore-Then-Commit} \end{lemma} \begin{proof} - \uses{lem:iid_altReward, lem:independent_altReward, lem:sum_altReward, thm:hoeffding} + \uses{lem:iid_rewardByCount, lem:independent_rewardByCount, lem:sum_rewardByCount, thm:hoeffding} \begin{align*} \mathbb{P}(\hat{A}_m^* = a) &\le \mathbb{P}(\hat{\mu}_a \ge \hat{\mu}_{a^*}) @@ -48,7 +48,7 @@ \section{Explore-Then-Commit} &= \mathbb{P}\left(\frac{1}{m} \sum_{t=0}^{Km-1} \mathbb{I}(A_t = a) X_t \ge \frac{1}{m} \sum_{t=0}^{Km-1} \mathbb{I}(A_t = a^*) X_t\right) \: . \end{align*} -By Lemma~\ref{lem:sum_altReward}, the empirical means are means of $m$ i.i.d. samples $Y_{a,i}$ and $Y_{a^*,i}$ from the distributions $\nu(a)$ and $\nu(a^*)$. +By Lemma~\ref{lem:sum_rewardByCount}, the empirical means are means of $m$ i.i.d. samples $Y_{a,i}$ and $Y_{a^*,i}$ from the distributions $\nu(a)$ and $\nu(a^*)$. \begin{align*} &= \mathbb{P}\left(\frac{1}{m} \sum_{i=1}^m Y_{a,i} \ge \frac{1}{m} \sum_{i=1}^m Y_{a^*,i}\right) \\ From 2119ea22215d98b7e21c12ebf22ced9e09a28716 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 4 Sep 2025 11:35:28 +0200 Subject: [PATCH 4/4] add stream to the probability space --- blueprint/src/chapters/bandit.tex | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 2275f9b1..ff2faeb7 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -38,19 +38,21 @@ \section{Algorithm, bandit and probability space} \uses{def:algorithm, def:bandit} \leanok \lean{Bandits.Bandit.measure} -By an application of the Ionescu-Tulcea theorem, an algorithm $(\pi, P_0)$ and bandit $\nu$ together defines a probability distribution on the space $\Omega := (\mathcal{A} \times \mathbb{R})^{\mathbb{N}}$, the space of infinite sequences of arms and rewards. -We denote that distribution by $\mathbb{P}$. -TODO: explain how the probability distribution is constructed. +By an application of the Ionescu-Tulcea theorem, an algorithm $(\pi, P_0)$ and bandit $\nu$ together defines a probability distribution $\mathbb{P}_B$ on the space $\Omega_B := (\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_B \times \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$ and $\mathbb{P} = \mathbb{P}_B \otimes (\bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a))$. + +TODO: explain how the probability distribution $\mathbb{P}_B$ is constructed. \end{definition} +The reason for adding the extra stream of rewards is explained in Section~\ref{sec:alt_model}. \begin{definition}[Arms, rewards and history]\label{def:armAndReward} \leanok \lean{Bandits.arm, Bandits.reward, Bandits.hist} For $t \in \mathbb{N}$, we denote by $A_t$ the arm pulled at time $t$ and by $X_t$ the reward received at time $t$. -Formally, these are measurable functions on $\Omega = (\mathcal{A} \times \mathbb{R})^{\mathbb{N}}$, defined by $A_t(\omega) = \omega_{t,1}$ and $X_t(\omega) = \omega_{t,2}$. +Formally, these are measurable functions on $\Omega = (\mathcal{A} \times \mathbb{R})^{\mathbb{N}} \times \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$, defined by $A_t(\omega) = \omega_{1,t,1}$ and $X_t(\omega) = \omega_{1,t,2}$. We denote by $H_t \in (\mathcal{A} \times \mathbb{R})^{t+1}$ the history of pulls and rewards up to and including time $t$, that is $H_t = ((A_0, X_0), \ldots, (A_t, X_t))$. -Formally, $H_t(\omega) = (\omega_0, \ldots, \omega_t)$. +Formally, $H_t(\omega) = (\omega_{1,0}, \ldots, \omega_{1,t})$. \end{definition} @@ -101,7 +103,7 @@ \section{Algorithm, bandit and probability space} -\section{Alternative model} +\section{Alternative model}\label{sec:alt_model} The description of the bandit model above considers that at time $t$, a reward $X_t$ is generated, depending on the arm $A_t$ pulled at that time. An alternative way to talk about that process is to imagine that there is a stream of rewards from each arm, and that the algorithm sees the first, then second, etc. reward from the arms at it pulls them. @@ -120,11 +122,11 @@ \section{Alternative model} \uses{def:stepsUntil} \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. +For $a \in \mathcal{A}$ and $n \in \mathbb{N}$, let $Z_{n,a} \sim \nu(a)$, independent of the bandit interaction and other $Z_{m,b}$. +In our probability space $\Omega$, we can take for $Z_{n,a}$ the function $\omega \mapsto \omega_{2,n,a}$. 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} -TODO: that definition requires changing the probability space to $\Omega \times \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$. \begin{lemma}\label{lem:iid_rewardByCount} \uses{def:rewardByCount} @@ -154,7 +156,7 @@ \section{Alternative model} \end{lemma} \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$. +By definition, $T_{N_{t+1,a}, a} = \min\{s \in \mathbb{N} \mid N_{s+1,a} = N_{t+1,a}\} \le t < \infty$. \end{proof}