diff --git a/blueprint/lean_decls b/blueprint/lean_decls
index b9510cbe..b293750c 100644
--- a/blueprint/lean_decls
+++ b/blueprint/lean_decls
@@ -100,6 +100,15 @@ ProbabilityTheory.HasSubgaussianMGF.add_of_indepFun
 ProbabilityTheory.HasSubgaussianMGF.measure_ge_le
 ProbabilityTheory.HasSubgaussianMGF.measure_sum_range_ge_le_of_iIndepFun
 ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le'
+Bandits.ArrayModel.identDistrib_pullCount_prod_sumRewards
+Bandits.ArrayModel.identDistrib_sum_range_snd
+Bandits.ArrayModel.prob_pullCount_prod_sumRewards_mem_le
+Bandits.prob_pullCount_prod_sumRewards_mem_le
+Bandits.ArrayModel.prob_sumRewards_le_sumRewards_le
+Bandits.probReal_sumRewards_le_sumRewards_le
+Bandits.probReal_sum_le_sum_streamMeasure
+Bandits.prob_sum_le_sqrt_log
+Bandits.prob_sum_ge_sqrt_log
 Bandits.ETC.nextArm
 Bandits.etcAlgorithm
 Bandits.ETC.pullCount_of_ge
diff --git a/blueprint/src/appendix/conditional_independence.tex b/blueprint/src/appendix/conditional_independence.tex
index 481dd197..14a678bd 100644
--- a/blueprint/src/appendix/conditional_independence.tex
+++ b/blueprint/src/appendix/conditional_independence.tex
@@ -7,7 +7,7 @@ \chapter{Conditional independence}
 If $X \ind Y \mid Z$, then $X \ind (Y, Z) \mid Z$.
 \end{lemma}
 
-\begin{proof}
+\begin{proof}\leanok
 
 \end{proof}
 
diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex
index 576e03b2..d377caf3 100644
--- a/blueprint/src/chapters/bandit.tex
+++ b/blueprint/src/chapters/bandit.tex
@@ -418,18 +418,14 @@ \subsection{Laws}
 \end{proof}
 
 
-\section{Alternative models: rewards indexed by time or pull count}\label{sec:alt_model}
 
-The description of the bandit model above considers that at time $t$, a reward $R_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.
-This uses the random variables $Y_{n, a}$ defined in Definition~\ref{def:rewardByCount}, which represent the $n^{th}$ reward obtained from arm $a$.
-We now describe the distribution of those rewards.
 
-The probability space $\Omega_{\mathcal{T}}$ has been augmented with $\Omega' = \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$, on which we put the product measure $\bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a)$.
-With that measure, the law of $Z_{n,a}$ is $\nu(a)$.
+\section{Law of the n\textsuperscript{th} pull}\label{sec:alt_model}
+
+This section describes the law of $Y_{n, a}$ the $n^{th}$ reward obtained from an arm $a \in \mathcal{A}$ (Definition~\ref{def:rewardByCount}).
 
-Our main goal in this section is to prove that $(Y_{n,a})_{n \in \mathbb{N}, a \in \mathcal{A}}$ and $(Z_{n,a})_{n \in \mathbb{N}, a \in \mathcal{A}}$ are identically distributed.
-This can be done by proving that for each $n$ and $a$, $Y_{n,a}$ and $Z_{n,a}$ are identically distributed (with law $\nu(a)$), and that the family $(Y_{n,a})_{n \in \mathbb{N}, a \in \mathcal{A}}$ is independent.
+We augment the probability space $\Omega$ on which we have an algorithm-environment sequence with $\Omega' = \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$, on which we put the product measure $\bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a)$.
+With that measure, the law of $Z_{n,a}$ is $\nu(a)$.
 
 
 \begin{lemma}\label{lem:measurable_comap_indicator_stepsUntil_eq}
@@ -525,116 +521,116 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al
 \end{proof}
 
 
-\begin{lemma}\label{lem:indepFun_rewardByCount_stepsUntil}
-  \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure}
-For $n > 0$, $Y_{n, a} \ind T_{n,a}$.
-\end{lemma}
+% \begin{lemma}\label{lem:indepFun_rewardByCount_stepsUntil}
+%   \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure}
+% For $n > 0$, $Y_{n, a} \ind T_{n,a}$.
+% \end{lemma}
 
-\begin{proof}
-  \uses{lem:condDistrib_rewardByCount_stepsUntil, lem:hasLaw_rewardByCount}
-It suffices to prove that $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \mathcal{L}(Y_{n,a})$.
+% \begin{proof}
+%   \uses{lem:condDistrib_rewardByCount_stepsUntil, lem:hasLaw_rewardByCount}
+% It suffices to prove that $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \mathcal{L}(Y_{n,a})$.
 
-By Lemma~\ref{lem:hasLaw_rewardByCount}, $\mathcal{L}(Y_{n,a}) = \nu(a)$.
-By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \nu(a)$.
-\end{proof}
+% By Lemma~\ref{lem:hasLaw_rewardByCount}, $\mathcal{L}(Y_{n,a}) = \nu(a)$.
+% By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \nu(a)$.
+% \end{proof}
 
 
-\begin{lemma}\label{lem:condIndepFun_rewardByCount_hist}
-  \uses{def:rewardByCount, def:stepsUntil, def:Bandit.measure}
-For $n > 0$, $Y_{n, a} \ind H_{T_{n,a}-1} \mid T_{n,a}$, in which $H_{\infty}$ is interpreted as the whole history.
-\end{lemma}
+% \begin{lemma}\label{lem:condIndepFun_rewardByCount_hist}
+%   \uses{def:rewardByCount, def:stepsUntil, def:Bandit.measure}
+% For $n > 0$, $Y_{n, a} \ind H_{T_{n,a}-1} \mid T_{n,a}$, in which $H_{\infty}$ is interpreted as the whole history.
+% \end{lemma}
 
-\begin{proof}
-  \uses{lem:condDistrib_rewardByCount_stepsUntil, lem:condIndepFun_reward_hist_action}
-By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \nu(a)$.
-We need to prove that $\mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a}) = \nu(a)$.
-By Lemma~\ref{lem:stepsUntil_basic}, if $T_{n,a} = t \in \mathbb{N}$, then $A_t = a$.
-We get
-\begin{align*}
-  \mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a} = t)
-  &= \mathcal{L}(R_t \mid H_{t-1}, T_{n,a} = t, A_t = a)
-  \: .
-\end{align*}
-Then, $\mathbb{I}\{T_{n,a} = t\}$ is a function of $(H_{t-1}, A_t)$ by Lemma~\ref{lem:measurable_comap_indicator_stepsUntil_eq}, such that
+% \begin{proof}
+%   \uses{lem:condDistrib_rewardByCount_stepsUntil, lem:condIndepFun_reward_hist_action}
+% By Lemma~\ref{lem:condDistrib_rewardByCount_stepsUntil}, $\mathcal{L}(Y_{n,a} \mid T_{n,a}) = \nu(a)$.
+% We need to prove that $\mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a}) = \nu(a)$.
+% By Lemma~\ref{lem:stepsUntil_basic}, if $T_{n,a} = t \in \mathbb{N}$, then $A_t = a$.
+% We get
+% \begin{align*}
+%   \mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a} = t)
+%   &= \mathcal{L}(R_t \mid H_{t-1}, T_{n,a} = t, A_t = a)
+%   \: .
+% \end{align*}
+% Then, $\mathbb{I}\{T_{n,a} = t\}$ is a function of $(H_{t-1}, A_t)$ by Lemma~\ref{lem:measurable_comap_indicator_stepsUntil_eq}, such that
 
-\begin{align*}
-  \mathcal{L}(R_t \mid H_{t-1}, T_{n,a} = t, A_t = a)
-  &= \mathcal{L}(R_t \mid H_{t-1}, A_t = a)
-  \: .
-\end{align*}
-Thus, using Lemma~\ref{lem:condIndepFun_reward_hist_action}, we have
-\begin{align*}
-  \mathcal{L}(R_t \mid H_{t-1}, A_t = a)
-  = \nu(a)
-  \: .
-\end{align*}
+% \begin{align*}
+%   \mathcal{L}(R_t \mid H_{t-1}, T_{n,a} = t, A_t = a)
+%   &= \mathcal{L}(R_t \mid H_{t-1}, A_t = a)
+%   \: .
+% \end{align*}
+% Thus, using Lemma~\ref{lem:condIndepFun_reward_hist_action}, we have
+% \begin{align*}
+%   \mathcal{L}(R_t \mid H_{t-1}, A_t = a)
+%   = \nu(a)
+%   \: .
+% \end{align*}
 
-If $T_{n,a} = \infty$, then $\mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a} = \infty) = \mathcal{L}(Z_{n,a} \mid H_{\infty}, T_{n,a} = \infty) = \nu(a)$ by independence of $Z_{n,a}$ from the history and $T_{n,a}$.
+% If $T_{n,a} = \infty$, then $\mathcal{L}(Y_{n,a} \mid H_{T_{n,a}-1}, T_{n,a} = \infty) = \mathcal{L}(Z_{n,a} \mid H_{\infty}, T_{n,a} = \infty) = \nu(a)$ by independence of $Z_{n,a}$ from the history and $T_{n,a}$.
 
-\end{proof}
+% \end{proof}
 
 
-\begin{lemma}\label{lem:indepFun_rewardByCount_hist_stepsUntil}
-  \uses{def:rewardByCount, def:stepsUntil, def:Bandit.measure}
-For $n > 0$, $Y_{n, a} \ind (H_{T_{n,a}-1}, T_{n,a})$.
-\end{lemma}
+% \begin{lemma}\label{lem:indepFun_rewardByCount_hist_stepsUntil}
+%   \uses{def:rewardByCount, def:stepsUntil, def:Bandit.measure}
+% For $n > 0$, $Y_{n, a} \ind (H_{T_{n,a}-1}, T_{n,a})$.
+% \end{lemma}
 
-\begin{proof}
-  \uses{lem:condIndepFun_rewardByCount_hist}
-By Lemma~\ref{lem:condIndepFun_rewardByCount_hist}, $Y_{n, a} \ind H_{T_{n,a}-1} \mid T_{n,a}$.
-By Lemma~\ref{lem:indepFun_rewardByCount_stepsUntil}, $Y_{n, a} \ind T_{n,a}$.
-By the contraction property of conditional independence (Lemma~\ref{lem:indepFun_contraction}), we have $Y_{n, a} \ind (H_{T_{n,a}-1}, T_{n,a})$.
-\end{proof}
+% \begin{proof}
+%   \uses{lem:condIndepFun_rewardByCount_hist}
+% By Lemma~\ref{lem:condIndepFun_rewardByCount_hist}, $Y_{n, a} \ind H_{T_{n,a}-1} \mid T_{n,a}$.
+% By Lemma~\ref{lem:indepFun_rewardByCount_stepsUntil}, $Y_{n, a} \ind T_{n,a}$.
+% By the contraction property of conditional independence (Lemma~\ref{lem:indepFun_contraction}), we have $Y_{n, a} \ind (H_{T_{n,a}-1}, T_{n,a})$.
+% \end{proof}
 
 
-\begin{lemma}\label{lem:iIndepFun_rewardByCount}
-  \uses{def:rewardByCount}
-The rewards $(Y_{n,a})_{n \in \mathbb{N}}$ are independent.
-\end{lemma}
+% \begin{lemma}\label{lem:iIndepFun_rewardByCount}
+%   \uses{def:rewardByCount}
+% The rewards $(Y_{n,a})_{n \in \mathbb{N}}$ are independent.
+% \end{lemma}
 
-\begin{proof}
-  \uses{lem:iIndepFun_nat_iff_forall_indepFun, lem:indepFun_contraction, lem:indepFun_rewardByCount_stepsUntil}
-By Lemma~\ref{lem:iIndepFun_nat_iff_forall_indepFun}, it suffices to show that for all $n \in \mathbb{N}$, $Y_{n+1, a}$ is independent of $(Y_{1,a}, \ldots, Y_{n,a})$.
+% \begin{proof}
+%   \uses{lem:iIndepFun_nat_iff_forall_indepFun, lem:indepFun_contraction, lem:indepFun_rewardByCount_stepsUntil}
+% By Lemma~\ref{lem:iIndepFun_nat_iff_forall_indepFun}, it suffices to show that for all $n \in \mathbb{N}$, $Y_{n+1, a}$ is independent of $(Y_{1,a}, \ldots, Y_{n,a})$.
 
-By the contraction property of conditional independence (Lemma~\ref{lem:indepFun_contraction}), it suffices to show that $Y_{n+1, a}$ is independent of $(Y_{1,a}, \ldots, Y_{n,a})$ conditionally on $T_{n+1, a}$ and that $Y_{n+1, a}$ is independent of $T_{n+1, a}$.
+% By the contraction property of conditional independence (Lemma~\ref{lem:indepFun_contraction}), it suffices to show that $Y_{n+1, a}$ is independent of $(Y_{1,a}, \ldots, Y_{n,a})$ conditionally on $T_{n+1, a}$ and that $Y_{n+1, a}$ is independent of $T_{n+1, a}$.
 
-The fact that $Y_{n+1, a}$ is independent of $T_{n+1, a}$ is Lemma~\ref{lem:indepFun_rewardByCount_stepsUntil}.
+% The fact that $Y_{n+1, a}$ is independent of $T_{n+1, a}$ is Lemma~\ref{lem:indepFun_rewardByCount_stepsUntil}.
 
-TODO
+% TODO
 
-\end{proof}
+% \end{proof}
 
 
-\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}
+% \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}
 
-\begin{proof}
+% \begin{proof}
 
-\end{proof}
+% \end{proof}
 
 
-\begin{lemma}\label{lem:identDistrib_rewardByCount_stream}
-  \uses{def:rewardByCount}
-The random sequences $(Y_{n+1,a})_{n \in \mathbb{N}}$ and $(Z_{n,a})_{n \in \mathbb{N}}$ are identically distributed.
-\end{lemma}
+% \begin{lemma}\label{lem:identDistrib_rewardByCount_stream}
+%   \uses{def:rewardByCount}
+% The random sequences $(Y_{n+1,a})_{n \in \mathbb{N}}$ and $(Z_{n,a})_{n \in \mathbb{N}}$ are identically distributed.
+% \end{lemma}
 
-\begin{proof}
-  \uses{lem:hasLaw_rewardByCount, lem:iIndepFun_rewardByCount}
+% \begin{proof}
+%   \uses{lem:hasLaw_rewardByCount, lem:iIndepFun_rewardByCount}
 
-\end{proof}
+% \end{proof}
 
 
-\begin{lemma}\label{lem:identDistrib_sum_Icc_rewardByCount}
-  \uses{def:rewardByCount}
-The random variables $\sum_{i=1}^n Y_{i,a}$ and $\sum_{i=0}^{n-1} Z_{i,a}$ are identically distributed.
-\end{lemma}
+% \begin{lemma}\label{lem:identDistrib_sum_Icc_rewardByCount}
+%   \uses{def:rewardByCount}
+% The random variables $\sum_{i=1}^n Y_{i,a}$ and $\sum_{i=0}^{n-1} Z_{i,a}$ are identically distributed.
+% \end{lemma}
 
-\begin{proof}
-  \uses{lem:identDistrib_rewardByCount_stream}
-Immediate consequence of Lemma~\ref{lem:identDistrib_rewardByCount_stream}.
-\end{proof}
+% \begin{proof}
+%   \uses{lem:identDistrib_rewardByCount_stream}
+% Immediate consequence of Lemma~\ref{lem:identDistrib_rewardByCount_stream}.
+% \end{proof}
 
 
 \section{Regret and other bandit quantities}
diff --git a/blueprint/src/chapters/concentration.tex b/blueprint/src/chapters/concentration.tex
index 6ef370c1..8f58b037 100644
--- a/blueprint/src/chapters/concentration.tex
+++ b/blueprint/src/chapters/concentration.tex
@@ -1,5 +1,8 @@
 \chapter{Concentration inequalities}
 
+
+\section{Sub-Gaussian random variables}
+
 \begin{definition}[Sub-Gaussian]\label{def:subGaussian}
   \mathlibok
   \lean{ProbabilityTheory.HasSubgaussianMGF}
@@ -79,3 +82,116 @@ \chapter{Concentration inequalities}
   \uses{lem:subGaussian_add_of_indepFun, thm:hoeffding}
 
 \end{proof}
+
+
+
+
+\section{Laws of sums of rewards}
+
+
+\begin{lemma}\label{lem:AM.identDistrib_pullCount_prod_sumRewards}
+  \uses{def:rewardByCount, def:sumRewards, def:pullCount, def:AM.history}
+  \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}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:AM.identDistrib_sum_range_snd}
+  \uses{def:AM.history}
+  \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)$.
+\end{lemma}
+
+\begin{proof}\leanok
+By definition of $P_{\mathcal{A}}$ (Definition~\ref{def:arrayMeasure}).
+\end{proof}
+
+
+\begin{lemma}\label{lem:prob_pullCount_prod_sumRewards_mem_le}
+  \uses{def:sumRewards, def:pullCount, def:AM.history}
+  \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}$,
+\begin{align*}
+  P_{\mathcal{A}}\left((N_{t,a}, S_{t, a}) \in B\right)
+  &\le \sum_{k < t, \exists r, (k, r) \in B} \nu(a)^{\otimes \mathbb{N}} \left(\sum_{s=0}^{k-1} \omega_{s} \in \{x \mid \exists n, (n, x) \in B\}\right)
+  \: .
+\end{align*}
+As a consequence, this also holds for any algorithm-environment sequence.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.identDistrib_pullCount_prod_sumRewards, lem:AM.identDistrib_sum_range_snd, thm:isAlgEnvSeq_unique, thm:isAlgEnvSeq_arrayMeasure}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:prob_sumRewards_le_sumRewards_le}
+  \uses{def:sumRewards, def:pullCount, def:AM.history}
+  \leanok
+  \lean{Bandits.ArrayModel.prob_sumRewards_le_sumRewards_le, Bandits.probReal_sumRewards_le_sumRewards_le}
+In the array model,
+\begin{align*}
+  P_{\mathcal{A}}\left( N_{t, a^*} = m_1 \wedge N_{t, a} = m_2 \wedge S_{t, a^*} \le S_{t, a}\right)
+  &\le (\otimes_a \nu(a))^{\otimes \mathbb{N}} \left( \sum_{s=0}^{m_1-1} \omega_{s, a^*} \le \sum_{s=0}^{m_2-1} \omega_{s, a} \right)
+  \: .
+\end{align*}
+As a consequence, this also holds for any algorithm-environment sequence.
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:AM.identDistrib_pullCount_prod_sumRewards, lem:AM.identDistrib_sum_range_snd, thm:isAlgEnvSeq_unique,thm:isAlgEnvSeq_arrayMeasure}
+
+\end{proof}
+
+
+
+\subsection{Sub-Gaussian rewards}
+
+
+\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)
+\end{align*}
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{lem:measure_sum_le_sum_le'}
+
+\end{proof}
+
+
+\begin{lemma}\label{lem:prob_sum_le_sqrt_log}
+  \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}$.
+Let $c \ge 0$ be a real number and $k$ a positive natural number.
+Then
+\begin{align*}
+  \nu(a)^{\otimes \mathbb{N}} \left( \sum_{s=0}^{k-1} (\omega_{s} - \mu_a) \le - \sqrt{c k \log(n + 1)} \right)
+  &\le \frac{1}{(n + 1)^{c / 2}}
+  \: .
+\end{align*}
+The same upper bound holds for the upper tail:
+\begin{align*}
+  \nu(a)^{\otimes \mathbb{N}} \left( \sum_{s=0}^{k-1} (\omega_{s} - \mu_a) \ge \sqrt{c k \log(n + 1)} \right)
+  &\le \frac{1}{(n + 1)^{c / 2}}
+  \: .
+\end{align*}
+\end{lemma}
+
+\begin{proof}\leanok
+  \uses{thm:hoeffding}
+
+\end{proof}
diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex
index 50e82c48..176e2909 100644
--- a/blueprint/src/chapters/etc.tex
+++ b/blueprint/src/chapters/etc.tex
@@ -1,5 +1,7 @@
 \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.
diff --git a/blueprint/src/chapters/ucb.tex b/blueprint/src/chapters/ucb.tex
index 54ffc48a..786b5bf3 100644
--- a/blueprint/src/chapters/ucb.tex
+++ b/blueprint/src/chapters/ucb.tex
@@ -1,5 +1,7 @@
 \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