Blueprint update: ETC and UCB (#56)

Author: RemyDegenne

blueprint/lean_decls

@@ -120,8 +120,6 @@ Bandits.ucbAlgorithm
 Bandits.UCB.ucbIndex_le_ucbIndex_arm
 Bandits.UCB.gap_arm_le_two_mul_ucbWidth
 Bandits.UCB.pullCount_arm_le
-Bandits.UCB.todo
-Bandits.UCB.todo'
 Bandits.UCB.prob_ucbIndex_le
 Bandits.UCB.prob_ucbIndex_ge
 Bandits.UCB.pullCount_le_add_three

blueprint/src/chapters/algorithm.tex

@@ -73,6 +73,7 @@ \chapter{Iterative stochastic algorithms}
 For such a statement to make sense, we need a probability space on which the whole sequence of actions and observations is defined as a random variable.
 
 We denote by $P[X \mid Y]$ the conditional distribution of a random variable $X$ given another random variable $Y$ under a probability measure $P$.
+When we write that $P[X \mid Y] = \kappa$, or that $X$ has conditional distribution $\kappa$ given $Y$, the equality should be understood as holding $Y_* P$-almost surely.
 
 
 \begin{definition}[Algorithm-environment interaction]\label{def:IsAlgEnvSeq}
@@ -229,7 +230,7 @@ \subsection{Ionescu-Tulcea theorem}
 $(\mathcal{F}_t)_{t \in \mathbb{N}}$ is the canonical filtration on $\Omega_{\mathcal{T}}$, and is the natural filtration for the canonical process $(X_t)_{t \in \mathbb{N}}$.
 
 
-\begin{lemma}\label{lem:adapted_history}
+\begin{lemma}\label{lem:IT.adapted_history}
   \uses{def:IT.history, def:IT.filtration}
   \leanok
   \lean{Learning.IT.adapted_step, Learning.IT.adapted_hist}
@@ -242,7 +243,7 @@ \subsection{Ionescu-Tulcea theorem}
 \end{proof}
 
 
-\begin{lemma}\label{lem:condDistrib_X_add_one}
+\begin{lemma}\label{lem:IT.condDistrib_X_add_one}
   \uses{def:IT.history, def:trajMeasure}
   \leanok
   \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure}
@@ -256,7 +257,7 @@ \subsection{Ionescu-Tulcea theorem}
 \end{proof}
 
 
-\begin{lemma}\label{lem:law_X_zero}
+\begin{lemma}\label{lem:IT.law_X_zero}
   \uses{def:IT.history, def:trajMeasure}
   \leanok
   \lean{Learning.IsAlgEnvSeq.hasLaw_step_zero}
@@ -286,7 +287,7 @@ \subsection{Case of an algorithm-environment interaction}
 \end{definition}
 
 
-\begin{lemma}\label{lem:adapted_action_reward}
+\begin{lemma}\label{lem:IT.adapted_action_reward}
   \uses{def:IT.actionReward, def:IT.filtration}
   \leanok
   \lean{Learning.IT.adapted_action, Learning.IT.adapted_reward}
@@ -295,72 +296,72 @@ \subsection{Case of an algorithm-environment interaction}
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:adapted_history}
+  \uses{lem:IT.adapted_history}
 
 \end{proof}
 
 
 We need to check that the random variables $A_t$ and $R_t$ have the expected conditional distributions.
 
-\begin{lemma}\label{lem:condDistrib_A_add_one}
+\begin{lemma}\label{lem:IT.condDistrib_A_add_one}
   \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment}
   \leanok
   \lean{Learning.IT.condDistrib_action}
 For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\pi_t$.
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:condDistrib_X_add_one}
-By Lemma~\ref{lem:condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \pi_t \otimes \nu_t$.
+  \uses{lem:IT.condDistrib_X_add_one}
+By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \pi_t \otimes \nu_t$.
 Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}_{t+1}$, $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}_{t+1}$, which is $\pi_t$.
 \end{proof}
 
 
-\begin{lemma}\label{lem:condDistrib_R_add_one}
+\begin{lemma}\label{lem:IT.condDistrib_R_add_one}
   \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment}
   \leanok
   \lean{Learning.IT.condDistrib_reward}
 For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[R_{t+1} \mid H_t, A_{t+1}\right]$ is $((H_t, A_{t+1})_* P_{\mathcal{T}})$-almost surely equal to $\nu_t$.
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:condDistrib_X_add_one, lem:condDistrib_A_add_one}
+  \uses{lem:IT.condDistrib_X_add_one, 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:condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \pi_t \otimes \nu_t$.
+By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t = \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}}$.
 
 We thus have to prove that $((H_t)_* P_{\mathcal{T}}) \otimes (\pi_t \otimes \nu_t) = ((H_t, A_{t+1})_* P_{\mathcal{T}}) \otimes \nu_t$.
 
-By Lemma~\ref{lem:condDistrib_A_add_one}, $(H_t, A_{t+1})_* P_{\mathcal{T}} = (H_t)_* P_{\mathcal{T}} \otimes \pi_t$, and replacing this in the right-hand side gives the left-hand side (using associativity of the composition-product).
+By Lemma~\ref{lem:IT.condDistrib_A_add_one}, $(H_t, A_{t+1})_* P_{\mathcal{T}} = (H_t)_* P_{\mathcal{T}} \otimes \pi_t$, and replacing this in the right-hand side gives the left-hand side (using associativity of the composition-product).
 \end{proof}
 
 
-\begin{lemma}\label{lem:law_A_zero}
+\begin{lemma}\label{lem:IT.law_A_zero}
   \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment}
   \leanok
   \lean{Learning.IT.hasLaw_action_zero}
 The law of $A_0$ under $P_{\mathcal{T}}$ is $\alpha_0$.
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:law_X_zero}
+  \uses{lem:IT.law_X_zero}
 $X_0$ has law $\mu = \alpha_0 \otimes \nu'_0$. $A_0$ is the projection of $X_0$ on the first space $\mathcal{A}_0$ and $\nu_0'$ is Markov, so $A_0$ has law $\alpha_0$.
 \end{proof}
 
 
-\begin{lemma}\label{lem:condDistrib_R_zero}
+\begin{lemma}\label{lem:IT.condDistrib_R_zero}
   \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment}
   \leanok
   \lean{Learning.IT.condDistrib_reward_zero}
 The conditional distribution $P_{\mathcal{T}}\left[R_0 \mid A_0\right]$ is $(A_{0*} P_{\mathcal{T}})$-almost surely equal to $\nu'_0$.
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:law_X_zero}
+  \uses{lem:IT.law_X_zero}
 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:law_X_zero}, $X_{0*} P_{\mathcal{T}} = \mu = \alpha_0 \otimes \nu'_0$.
-By Lemma~\ref{lem:law_A_zero}, $A_{0*} P_{\mathcal{T}} = \alpha_0$.
+By Lemma~\ref{lem:IT.law_X_zero}, $X_{0*} P_{\mathcal{T}} = \mu = \alpha_0 \otimes \nu'_0$.
+By Lemma~\ref{lem:IT.law_A_zero}, $A_{0*} P_{\mathcal{T}} = \alpha_0$.
 Thus the two sides are equal.
 \end{proof}
 
@@ -373,8 +374,8 @@ \subsection{Case of an algorithm-environment interaction}
 \end{theorem}
 
 \begin{proof}\leanok
-  \uses{lem:law_A_zero, lem:condDistrib_R_zero, lem:condDistrib_A_add_one, lem:condDistrib_R_add_one}
-The four conditions of Definition~\ref{def:IsAlgEnvSeq} are exactly the statements of Lemmas~\ref{lem:law_A_zero}, \ref{lem:condDistrib_R_zero}, \ref{lem:condDistrib_A_add_one} and \ref{lem:condDistrib_R_add_one}.
+  \uses{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}
 
 
@@ -510,14 +511,14 @@ \section{Finitely many actions}
 \end{proof}
 
 
-\begin{lemma}\label{lem:measurable_rewardByCount_mul_indicator}
-  \uses{def:rewardByCount, def:stepsUntil}
-$Y_{n, a} \mathbb{I}\{T_{n, a} < \infty\}$ is $\mathcal{F}_{T_{n, a}}$-measurable.
-\end{lemma}
+% \begin{lemma}\label{lem:measurable_rewardByCount_mul_indicator}
+%   \uses{def:rewardByCount, def:stepsUntil}
+% $Y_{n, a} \mathbb{I}\{T_{n, a} < \infty\}$ is $\mathcal{F}_{T_{n, a}}$-measurable.
+% \end{lemma}
 
-\begin{proof}
-It is the stopped value of the adapted process $(R_t)_{t \in \mathbb{N}}$ at the stopping time $T_{n, a}$.
-\end{proof}
+% \begin{proof}
+% It is the stopped value of the adapted process $(R_t)_{t \in \mathbb{N}}$ at the stopping time $T_{n, a}$.
+% \end{proof}
 
 
 \section{Scalar rewards}

blueprint/src/chapters/concentration.tex

@@ -86,7 +86,7 @@ \section{Sub-Gaussian random variables}
 
 
 
-\section{Laws of sums of rewards}
+\section{Concentration of the sums of rewards in bandit models}
 
 
 \begin{lemma}\label{lem:AM.identDistrib_pullCount_prod_sumRewards}
@@ -155,14 +155,15 @@ \section{Laws of sums of rewards}
 
 \subsection{Sub-Gaussian rewards}
 
+TODO: extend this to sub-Gaussian with constant other than 1.
 
 \begin{lemma}\label{lem:probReal_sum_le_sum_streamMeasure}
   \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}$.
 \begin{align*}
   (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right)
-  &\le \exp\left( -m \frac{\Delta_a^2}{4 \sigma^2} \right)
+  &\le \exp\left( -m \frac{\Delta_a^2}{4} \right)
 \end{align*}
 \end{lemma}
 

blueprint/src/chapters/etc.tex

@@ -1,7 +1,5 @@
 \chapter{Bandit algorithms}
 
-TODO: update this chapter to reflect the changes in the formalization.
-
 \section{Explore-Then-Commit}
 
 Note: times start at 0 to be consistent with Lean.
@@ -58,28 +56,19 @@ \section{Explore-Then-Commit}
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:independent_rewardByCount, lem:sum_rewardByCount, lem:measure_sum_le_sum_le', lem:identDistrib_sum_Icc_rewardByCount, lem:sumRewards_bestArm_le_of_arm_mul_eq}
+  \uses{lem:prob_sumRewards_le_sumRewards_le, lem:probReal_sum_le_sum_streamMeasure, lem:sumRewards_bestArm_le_of_arm_mul_eq}
 By Lemma~\ref{lem:sumRewards_bestArm_le_of_arm_mul_eq},
 \begin{align*}
   \mathbb{P}(\hat{A}_m^* = a)
   &\le \mathbb{P}(S_{Km, a} \ge S_{Km, a^*})
   \: .
 \end{align*}
-By Lemma~\ref{lem:sum_rewardByCount}, $S_{Km, a} = \sum_{i=1}^m Y_{a,i}$ and $S_{Km, a^*} = \sum_{i=1}^m Y_{a^*,i}$.
-And by Lemma~\ref{lem:identDistrib_sum_Icc_rewardByCount} and the independence lemma~\ref{lem:independent_rewardByCount}, the pair $(\sum_{i=1}^m Y_{a,i}, \sum_{i=1}^m Y_{a^*,i})$ has the same distribution as $(\sum_{i=0}^{m-1} Z_{i,a}, \sum_{i=0}^{m-1} Z_{i,a^*})$.
-We thus obtain
-\begin{align*}
-  \mathbb{P}(\hat{A}_m^* = a)
-  &\le \mathbb{P}\left(\sum_{i=0}^{m-1} Z_{i,a} \ge \sum_{i=0}^{m-1} Z_{i,a^*}\right)
-  \: .
-\end{align*}
-The random variables $Z_{i,a}$ and $Z_{i,a^*}$ are i.i.d. with distributions $\nu(a)$ and $\nu(a^*)$ respectively, and 1-sub-Gaussian by assumption.
-They satisfy the hypotheses of Lemma~\ref{lem:measure_sum_le_sum_le'}, and we thus obtain
+By Lemma~\ref{lem:prob_sumRewards_le_sumRewards_le}, and then the concentration inequality of Lemma~\ref{lem:probReal_sum_le_sum_streamMeasure} we have
 \begin{align*}
-  \mathbb{P}(\hat{A}_m^* = a)
-  &\le \mathbb{P}\left(\sum_{i=0}^{m-1} Z_{i,a} \ge \sum_{i=0}^{m-1} Z_{i,a^*}\right)
+  P_{\mathcal{A}}\left(S_{Km, a^*} \le S_{Km, a}\right)
+  &\le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m-1} \omega_{s, a^*} \le \sum_{s=0}^{m-1} \omega_{s, a} \right)
   \\
-  &\le \exp\left(- \frac{m \Delta_a^2}{4}\right)
+  &\le \exp\left( -m \frac{\Delta_a^2}{4} \right)
   \: .
 \end{align*}
 \end{proof}

blueprint/src/chapters/ucb.tex

@@ -1,7 +1,5 @@
 \section{UCB}
 
-TODO: update this chapter to reflect the changes in the formalization.
-
 \begin{definition}[UCB algorithm]\label{def:ucbAlgorithm}
   \uses{def:IT.actionReward, def:pullCount, def:empMean}
   \leanok
@@ -64,33 +62,6 @@ \section{UCB}
 \end{proof}
 
 
-%todo: move to concentration section?
-\begin{lemma}\label{lem:todo}
-  \uses{def:rewardByCount}
-  \leanok
-  \lean{Bandits.UCB.todo, Bandits.UCB.todo'}
-Suppose that $\nu(a)$ is 1-sub-Gaussian for all arms $a \in [K]$.
-Let $c \ge 0$ be a real number and $k$ a positive natural number.
-Then
-\begin{align*}
-  P\left(\frac{1}{k} \sum_{m=1}^k Y_{m, a} + \sqrt{\frac{c \log(n + 1)}{k}} \le \mu_a\right)
-  &\le \frac{1}{(n + 1)^{c / 2}}
-  \: .
-\end{align*}
-And also,
-\begin{align*}
-  P\left(\frac{1}{k} \sum_{m=1}^k Y_{m, a} - \sqrt{\frac{c \log(n + 1)}{k}} \ge \mu_a\right)
-  &\le \frac{1}{(n + 1)^{c / 2}}
-  \: .
-\end{align*}
-\end{lemma}
-
-\begin{proof}\leanok
-  \uses{lem:identDistrib_sum_Icc_rewardByCount, thm:hoeffding}
-
-\end{proof}
-
-
 \begin{lemma}\label{lem:prob_ucbIndex_le}
   \uses{def:empMean, def:pullCount}
   \leanok
@@ -112,10 +83,8 @@ \section{UCB}
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:todo, lem:pullCount_basic}
-Since $N_{n,a} \le n$ (Lemma~\ref{lem:pullCount_basic}), there exists $k \in [1, n]$ such that $N_{n,a} = k$ and $\hat{\mu}_{n,a} = \frac{1}{k} \sum_{m=1}^k Y_{m,a}$.
+  \uses{lem:prob_pullCount_prod_sumRewards_mem_le, lem:prob_sum_le_sqrt_log, lem:pullCount_basic}
 
-Then apply a union bound over $k \in [1, n]$ and use Lemma~\ref{lem:todo}.
 \end{proof}