From f16ea18d07513c81a2d8528bd5fffe317c5b8ca6 Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Fri, 16 Jan 2026 13:13:07 +0100 Subject: [PATCH] blueprint update: ETC and UCB --- blueprint/lean_decls | 2 - blueprint/src/chapters/algorithm.tex | 55 ++++++++++++------------ blueprint/src/chapters/concentration.tex | 5 ++- blueprint/src/chapters/etc.tex | 21 +++------ blueprint/src/chapters/ucb.tex | 33 +------------- 5 files changed, 37 insertions(+), 79 deletions(-) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index b293750c..ced961f0 100644 --- a/blueprint/lean_decls +++ b/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 diff --git a/blueprint/src/chapters/algorithm.tex b/blueprint/src/chapters/algorithm.tex index 044be591..9f0d03df 100644 --- a/blueprint/src/chapters/algorithm.tex +++ b/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,14 +296,14 @@ \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} @@ -310,13 +311,13 @@ \subsection{Case of an algorithm-environment interaction} \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} @@ -324,18 +325,18 @@ \subsection{Case of an algorithm-environment interaction} \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} @@ -343,12 +344,12 @@ \subsection{Case of an algorithm-environment interaction} \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} @@ -356,11 +357,11 @@ \subsection{Case of an algorithm-environment interaction} \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} diff --git a/blueprint/src/chapters/concentration.tex b/blueprint/src/chapters/concentration.tex index 8f58b037..c8fcee70 100644 --- a/blueprint/src/chapters/concentration.tex +++ b/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,6 +155,7 @@ \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 @@ -162,7 +163,7 @@ \subsection{Sub-Gaussian rewards} 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} diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex index 176e2909..e0c524c1 100644 --- a/blueprint/src/chapters/etc.tex +++ b/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} diff --git a/blueprint/src/chapters/ucb.tex b/blueprint/src/chapters/ucb.tex index 786b5bf3..6029a226 100644 --- a/blueprint/src/chapters/ucb.tex +++ b/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}