From 6ab07cdfa72a38f0fb96fd6faa2eff8dff9a296f Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 1 Jan 2026 09:36:06 +0100 Subject: [PATCH 1/3] bluprint update --- LeanBandits/Bandit/Bandit.lean | 2 +- blueprint/lean_decls | 70 ++++- blueprint/src/chapters/algorithm.tex | 310 +++++++++++++++++++++-- blueprint/src/chapters/bandit.tex | 254 +++++++------------ blueprint/src/chapters/concentration.tex | 21 ++ blueprint/src/chapters/etc.tex | 45 ++-- blueprint/src/chapters/ucb.tex | 197 ++++++++++++++ blueprint/src/content.tex | 1 - 8 files changed, 697 insertions(+), 203 deletions(-) diff --git a/LeanBandits/Bandit/Bandit.lean b/LeanBandits/Bandit/Bandit.lean index c31e3bb7..5e047baa 100644 --- a/LeanBandits/Bandit/Bandit.lean +++ b/LeanBandits/Bandit/Bandit.lean @@ -44,7 +44,7 @@ lemma snd_stepKernel (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel /-- Measure on the sequence of arms pulled and rewards observed generated by the bandit. -/ noncomputable def trajMeasure (alg : Algorithm α R) (ν : Kernel α R) [IsMarkovKernel ν] : Measure (ℕ → α × R) := - Kernel.trajMeasure (alg.p0 ⊗ₘ ν) (stepKernel alg ν) + Learning.trajMeasure alg (stationaryEnv ν) deriving IsProbabilityMeasure /-- Measure of an infinite stream of rewards from each arm. -/ diff --git a/blueprint/lean_decls b/blueprint/lean_decls index ab9b326e..8d7621e2 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -1,38 +1,84 @@ Learning.Algorithm Learning.Environment +Learning.detAlgorithm +Learning.stationaryEnv ProbabilityTheory.Kernel.traj ProbabilityTheory.Kernel.trajMeasure +Learning.step +Learning.hist +Learning.filtration +Learning.adapted_step +Learning.adapted_hist ProbabilityTheory.Kernel.condDistrib_trajMeasure +Learning.hasLaw_step_zero +Learning.action +Learning.reward +Learning.adapted_action +Learning.adapted_reward Learning.condDistrib_action Learning.condDistrib_reward Learning.hasLaw_action_zero Learning.condDistrib_reward_zero -Bandits.Bandit.measure -Bandits.arm -Bandits.reward -Bandits.hist +Learning.condDistrib_reward_stationaryEnv +Learning.condIndepFun_reward_hist_action Learning.pullCount -Bandits.filtration -Bandits.condDistrib_reward -Bandits.hasLaw_arm_zero -Bandits.condDistrib_arm +Learning.pullCount_zero +Learning.pullCount_mono +Learning.pullCount_add_one +Learning.pullCount_le +Learning.pullCount_congr +Learning.isPredictable_pullCount Learning.stepsUntil -Learning.rewardByCount -Bandits.hasLaw_rewardByCount -Bandits.iIndepFun_rewardByCount +Learning.stepsUntil_zero_of_ne +Learning.stepsUntil_zero_of_eq Learning.stepsUntil_pullCount_le Learning.stepsUntil_pullCount_eq +Learning.action_stepsUntil +Learning.pullCount_stepsUntil_add_one +Learning.pullCount_stepsUntil +Learning.isStoppingTime_stepsUntil +Learning.rewardByCount Learning.rewardByCount_pullCount_add_one_eq_reward +Learning.sumRewards +Learning.empMean Learning.sum_rewardByCount_eq_sumRewards +Bandits.Bandit.trajMeasure +Bandits.Bandit.measure +Bandits.measurable_comap_indicator_stepsUntil_eq +Bandits.condIndepFun_reward_hist_arm +Bandits.condIndepFun_reward_stepsUntil_arm +Bandits.reward_cond_stepsUntil +Bandits.condDistrib_rewardByCount_stepsUntil +Bandits.hasLaw_rewardByCount +Bandits.iIndepFun_rewardByCount' +Bandits.identDistrib_rewardByCount_stream +Bandits.identDistrib_sum_Icc_rewardByCount Bandits.regret Bandits.gap +Learning.sum_pullCount_mul 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 +ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le' Bandits.ETC.nextArm Bandits.etcAlgorithm Bandits.ETC.pullCount_of_ge +Bandits.ETC.sumRewards_bestArm_le_of_arm_mul_eq Bandits.ETC.prob_arm_mul_eq_le -Bandits.ETC.regret_le \ No newline at end of file +Bandits.ETC.regret_le +Bandits.UCB.nextArm +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 +Bandits.UCB.pullCount_le_add_three_ae +Bandits.UCB.some_sum_eq_zero +Bandits.UCB.expectation_pullCount_le +Bandits.UCB.regret_le \ No newline at end of file diff --git a/blueprint/src/chapters/algorithm.tex b/blueprint/src/chapters/algorithm.tex index 92edafdc..b91b8835 100644 --- a/blueprint/src/chapters/algorithm.tex +++ b/blueprint/src/chapters/algorithm.tex @@ -13,6 +13,7 @@ \chapter{Iterative stochastic algorithms} After the algorithm takes an action, the environment generates an observation according to a Markov kernel $\nu_t : (\mathcal{A} \times \mathcal{R})^{t+1} \times \mathcal{A} \rightsquigarrow \mathcal{R}$. + \begin{definition}[Environment]\label{def:environment} \leanok \lean{Learning.Environment} @@ -23,6 +24,28 @@ \chapter{Iterative stochastic algorithms} \end{itemize} \end{definition} + +\begin{definition}[Deterministic algorithm]\label{def:detAlgorithm} + \uses{def:algorithm} + \leanok + \lean{Learning.detAlgorithm} +An algorithm is deterministic if its initial probability measure $P_0$ is a Dirac measure and if all its policies $\pi_t$ are deterministic kernels. +\end{definition} + + +\begin{definition}[Stationary environment]\label{def:stationaryEnv} + \uses{def:environment} + \leanok + \lean{Learning.stationaryEnv} +An environment is stationary if there exists a Markov kernel $\nu : \mathcal{A} \rightsquigarrow \mathcal{R}$ such that $\nu'_0 = \nu$ and for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = \nu(a)$. +\end{definition} + + +\begin{remark}[Lean remark: properties vs constructors] +There are several ways to implement the last two definitions in Lean. We could write them as properties of algorithms and environments, or we can implement constructors that create algorithms and environments from the data in the definitions. We chose the latter option. Time will tell if it was a good choice. +\end{remark} + + Let's detail four examples of interactions between an algorithm and an environment. \begin{enumerate} \item \textbf{First order optimization}. The objective of the algorithm is to find the minimum of a function $f : \mathbb{R}^d \to \mathbb{R}$. @@ -36,12 +59,14 @@ \chapter{Iterative stochastic algorithms} \item \textbf{Adversarial bandits}. The action space is $\mathcal{A} = [K]$ for some $K \in \mathbb{N}$ (the set of arms) and the observation space is $\mathcal{R} = \mathbb{R}$ (the reward obtained after pulling an arm). The reward kernels are usually taken to be deterministic and in an \emph{oblivious} adversarial bandit they depend only on the time step: there is a sequence of vectors $(r_t)_{t \in \mathbb{N}}$ in $[0,1]^K$ such that for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = \delta_{r_{t,a}}$ (the Dirac measure at $r_{t,a}$). - \item \textbf{Reinforcement learnings in Markov decision processes}. + \item \textbf{Reinforcement learning in Markov decision processes}. TODO: main feature is that $\mathcal{R} = \mathcal{S} \times \mathbb{R}$ where $\mathcal{S}$ is the state space, and the kernel $\nu_t$ depends on the last state only. \end{enumerate} -\section{Ionescu-Tulcea theorem} + + +\section{Probability space: Ionescu-Tulcea theorem} If we group together the policy of the algorithm and the kernel of the environment at each time step, we get a sequence of Markov kernels $(\kappa_t)_{t \in \mathbb{N}}$, with $\kappa_t : (\mathcal{A} \times \mathcal{R})^{t+1} \rightsquigarrow (\mathcal{A} \times \mathcal{R})$. We will want to make global probabilistic statements about the whole sequence of actions and observations. @@ -65,7 +90,7 @@ \section{Ionescu-Tulcea theorem} The Ionescu-Tulcea theorem in Mathlib \cite{marion2025formalization} actually generates kernels $\xi_t : \prod_{s=0}^t \Omega_s \rightsquigarrow \prod_{s=0}^{\infty} \Omega_s$ for any $t$, with the property that the kernels are the identity on the first $t+1$ coordinates. -\begin{definition}\label{def:trajMeasure} +\begin{definition}[Trajectory measure]\label{def:trajMeasure} \uses{thm:ionescu-tulcea} \leanok \lean{ProbabilityTheory.Kernel.trajMeasure} @@ -75,16 +100,41 @@ \section{Ionescu-Tulcea theorem} \end{definition} -\begin{definition}\label{def:history} - \mathlibok % no need for a Lean definition +\begin{definition}[Step and history]\label{def:history} + \leanok + \lean{Learning.step, Learning.hist} For $t \in \mathbb{N}$, we denote by $X_t \in \Omega_t$ the random variable describing the time step $t$, and by $H_t \in \prod_{s=0}^t \Omega_s$ the history up to time $t$. Formally, these are measurable functions on $\Omega_{\mathcal{T}}$, defined by $X_t(\omega) = \omega_t$ and $H_t(\omega) = (\omega_1, \ldots, \omega_t)$. \end{definition} Note: $(X_t)_{t \in \mathbb{N}}$ is the canonical process on $\Omega_{\mathcal{T}}$. $H_t$ is equal to $\pi_{[0,t]}$. -We now list properties of those random variables that follow from the construction of the trajectory measure. +\begin{definition}[Filtration]\label{def:filtration} + \uses{def:history} + \leanok + \lean{Learning.filtration} +For $t \in \mathbb{N}$, we denote by $\mathcal{F}_t$ the sigma-algebra generated by the history up to time $t$: $\mathcal{F}_t = \sigma(H_t)$. +The family $(\mathcal{F}_t)_{t \in \mathbb{N}}$ is a filtration on $\Omega_{\mathcal{T}}$. +\end{definition} + +$(\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} + \uses{def:history, def:filtration} + \leanok + \lean{Learning.adapted_step, Learning.adapted_hist} +The random variables $X_t$ and $H_t$ are $\mathcal{F}_t$-measurable. +Said differently, the processes $(X_t)_{t \in \mathbb{N}}$ and $(H_t)_{t \in \mathbb{N}}$ are adapted to the filtration $(\mathcal{F}_t)_{t \in \mathbb{N}}$. +\end{lemma} + +\begin{proof}\leanok + +\end{proof} + + +We now list properties of those random variables that follow from the construction of the trajectory measure. We write $P[X \mid Y]$ for the conditional distribution of a random variable $X$ given another random variable $Y$ under a probability measure $P$. \begin{lemma}\label{lem:condDistrib_X_add_one} @@ -103,24 +153,52 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:law_X_zero} \uses{def:history, def:trajMeasure} + \leanok + \lean{Learning.hasLaw_step_zero} The law of $X_0$ under $P_{\mathcal{T}}$ is $\mu$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \end{proof} -\paragraph{Case of a composition-product} +\paragraph{Case of an algorithm-environment interaction.} -We suppose now that $\Omega_t = \mathcal{A}_t \times \mathcal{R}_t$ for some measurable spaces $\mathcal{A}_t$ and $\mathcal{R}_t$, and that for all $t \in \mathbb{N}$, $\kappa_t = \pi_t \otimes \nu_t$ for kernels $\pi_t : \prod_{s=0}^t(\mathcal{A}_s \times \mathcal{R}_s) \rightsquigarrow \mathcal{A}$ and $\nu_t : \prod_{s=0}^t(\mathcal{A}_s \times \mathcal{R}_s) \times \mathcal{A} \rightsquigarrow \mathcal{R}$. +We suppose now that, as in the algorithm-environment interaction, $\Omega_t = \mathcal{A}_t \times \mathcal{R}_t$ for some measurable spaces $\mathcal{A}_t$ and $\mathcal{R}_t$, and that for all $t \in \mathbb{N}$, $\kappa_t = \pi_t \otimes \nu_t$ for policy kernels $\pi_t : \prod_{s=0}^t(\mathcal{A}_s \times \mathcal{R}_s) \rightsquigarrow \mathcal{A}$ and feedback kernels $\nu_t : \prod_{s=0}^t(\mathcal{A}_s \times \mathcal{R}_s) \times \mathcal{A} \rightsquigarrow \mathcal{R}$. Likewise, $\mu = \alpha_0 \otimes \nu'_0$ for a probability measure $\alpha_0$ on $\mathcal{A}_0$ and a Markov kernel $\nu'_0 : \mathcal{A}_0 \rightsquigarrow \mathcal{R}_0$. -That's the case of an algorithm interacting with an environment as described above. +The step random variable $X_t$ takes values in $\mathcal{A}_t \times \mathcal{R}_t$. + +TODO: the code does not have $\mathcal{A}_t$ but a unique $\mathcal{A}$, same for $\mathcal{R}$. + +\begin{definition}\label{def:actionReward} + \uses{def:history} + \leanok + \lean{Learning.action, Learning.reward} We write $A_t$ and $R_t$ for the projections of $X_t$ on $\mathcal{A}_t$ and $\mathcal{R}_t$ respectively. +$A_t$ is the action taken at time $t$ and $R_t$ is the reward received at time $t$. +Formally, $A_t(\omega) = \omega_{t,1}$ and $R_t(\omega) = \omega_{t,2}$ for $\omega = \prod_{t=0}^{+\infty}(\omega_{t,1}, \omega_{t,2}) \in \prod_{t=0}^{+\infty} \mathcal{A}_t \times \mathcal{R}_t$. +\end{definition} + +\begin{lemma}\label{lem:adapted_action_reward} + \uses{def:actionReward, def:filtration} + \leanok + \lean{Learning.adapted_action, Learning.adapted_reward} +The random variables $A_t$ and $R_t$ are $\mathcal{F}_t$-measurable. +Said differently, the processes $(A_t)_{t \in \mathbb{N}}$ and $(R_t)_{t \in \mathbb{N}}$ are adapted to the filtration $(\mathcal{F}_t)_{t \in \mathbb{N}}$. +\end{lemma} + +\begin{proof}\leanok + \uses{lem: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} - \uses{def:history, def:trajMeasure, def:algorithm, def:environment} + \uses{def:actionReward, def:trajMeasure, def:algorithm, def:environment} \leanok \lean{Learning.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$. @@ -134,7 +212,7 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:condDistrib_R_add_one} - \uses{def:history, def:trajMeasure, def:algorithm, def:environment} + \uses{def:actionReward, def:trajMeasure, def:algorithm, def:environment} \leanok \lean{Learning.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$. @@ -153,7 +231,7 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:law_A_zero} - \uses{def:history, def:trajMeasure, def:algorithm, def:environment} + \uses{def:actionReward, def:trajMeasure, def:algorithm, def:environment} \leanok \lean{Learning.hasLaw_action_zero} The law of $A_0$ under $P_{\mathcal{T}}$ is $\alpha_0$. @@ -166,7 +244,7 @@ \section{Ionescu-Tulcea theorem} \begin{lemma}\label{lem:condDistrib_R_zero} - \uses{def:history, def:trajMeasure, def:algorithm, def:environment} + \uses{def:actionReward, def:trajMeasure, def:algorithm, def:environment} \leanok \lean{Learning.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$. @@ -183,7 +261,207 @@ \section{Ionescu-Tulcea theorem} +\section{Stationary environment} + +Recall that in a stationary environment, there exists a Markov kernel $\nu : \mathcal{A} \rightsquigarrow \mathcal{R}$ such that $\nu'_0 = \nu$ and for all $t \in \mathbb{N}$, for all $h_t \in (\mathcal{A} \times \mathcal{R})^{t+1}$, for all $a \in \mathcal{A}$, $\nu_t(h_t, a) = \nu(a)$. + + +\begin{lemma}\label{lem:condDistrib_reward_stationaryEnv} + \uses{def:actionReward, def:trajMeasure, def:algorithm, def:stationaryEnv} + \leanok + \lean{Learning.condDistrib_reward_stationaryEnv} +In a stationary environment, for any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\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:condDistrib_R_add_one, def:stationaryEnv} + +\end{proof} + + +\begin{lemma}\label{lem:condIndepFun_reward_hist_action} + \uses{def:actionReward, def:trajMeasure, def:algorithm, def:stationaryEnv} + \leanok + \lean{Learning.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}$. +\end{lemma} + +\begin{proof}\leanok + +\end{proof} + + + +\section{Finitely many actions} + +When the number of actions is finite, it makes sense to count how many times each action was chosen up to a certain time. +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: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\}$. +\end{definition} + +Note that the sum goes up to $t-1$, so that $N_{t,a}$ counts the number of times action $a$ was chosen \emph{before} time $t$. + + +\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 action 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 actions and rewards. +As a stochastic process, the empirical mean of an action is a function $\mathbb{N} \to (\mathcal{A} \times \mathcal{R})^{\mathbb{N}} \to \mathbb{R}$. + +Thus there are two similar but still 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} -\section{Independence and Markov property} -The structure of the sequence of kernels $(\kappa_t)_{t \in \mathbb{N}}$ is reflected in independence properties of the sequence of random variables $(X_t)_{t \in \mathbb{N}}$. +\begin{lemma}\label{lem:pullCount_basic} + \uses{def:pullCount, def:actionReward} + \leanok + \lean{Learning.pullCount_zero, Learning.pullCount_mono, Learning.pullCount_add_one, Learning.pullCount_le, Learning.pullCount_congr} +We note the following basic properties of $N_{t,a}$: +\begin{itemize} + \item $N_{0,a} = 0$. + \item $N_{t,a}$ is non-decreasing in $t$. + \item $N_{t + 1, A_t} = N_{t, A_t} + 1$ and for $a \ne A_t$, $N_{t + 1, a} = N_{t, a}$. + \item $N_{t, a} \le t$. + \item If for all $s \le t$, $A_s(\omega) = A_s(\omega')$, then $N_{t+1, a}(\omega) = N_{t+1, a}(\omega')$. +\end{itemize} +\end{lemma} + +\begin{proof}\leanok + +\end{proof} + + +\begin{lemma}\label{lem:predictable_pullCount} + \uses{def:filtration, def:pullCount} + \leanok + \lean{Learning.isPredictable_pullCount} +Let $a \in \mathcal{A}$. The process $(N_{t,a})_{t \in \mathbb{N}}$ is predictable with respect to the filtration $\mathcal{F}$. +\end{lemma} + +\begin{proof}\leanok + +\end{proof} + + +\begin{definition}\label{def:stepsUntil} + \uses{def:pullCount} + \leanok + \lean{Learning.stepsUntil} +For an action $a \in \mathcal{A}$ and a time $n \in \mathbb{N}$, we denote by $T_{n,a} \in \mathbb{N} \cup \{+\infty\}$ the time at which action $a$ was chosen for the $n$-th time, that is $T_{n,a} = \min\{s \in \mathbb{N} \mid N_{s+1,a} = n\}$. +Note that $T_{n, a}$ can be infinite if the action is not chosen $n$ times. +\end{definition} + +By definition, $T_{n, a}$ is the hitting time of the set $\{n\}$ by the process $t \mapsto N_{t+1,a}$, which is adapted since $N_{t,a}$ is predictable. +Equivalently, $T_{n, a}$ is the hitting time of the set $[n, +\infty]$ by that process. + + +\begin{lemma}\label{lem:stepsUntil_basic} + \uses{def:stepsUntil, def:pullCount} + \leanok + \lean{Learning.stepsUntil_zero_of_ne, Learning.stepsUntil_zero_of_eq, Learning.stepsUntil_pullCount_le, Learning.stepsUntil_pullCount_eq, Learning.action_stepsUntil, Learning.pullCount_stepsUntil_add_one, Learning.pullCount_stepsUntil} +We note the following basic properties of $T_{n,a}$: +\begin{itemize} + \item $T_{0,a} = 0$ for $a \ne A_0$. $T_{0,A_0} = \infty$. + \item $T_{N_{t+1, a}, a} \le t$. + \item $T_{N_{t + 1, A_t}, A_t} = t$. + \item If $T_{n, a} \ne \infty$ and $n > 0$, then $A_{T_{n, a}} = a$. + \item If $T_{n, a} \ne \infty$, then $N_{T_{n, a} + 1, a} = n$. + \item If $T_{n, a} \ne \infty$ and $n > 0$, then $N_{T_{n, a}, a} = n - 1$. + \item If for all $s \le t$, $A_s(\omega) = A_s(\omega')$, then $T_{n, a}(\omega) = t \iff T_{n, a}(\omega') = t$. +\end{itemize} +\end{lemma} + +\begin{proof}\leanok + +\end{proof} + + +\begin{lemma}\label{lem:isStoppingTime_stepsUntil} + \uses{def:filtration, def:stepsUntil} + \leanok + \lean{Learning.isStoppingTime_stepsUntil} +Let $a \in \mathcal{A}$. For any $n > 0$, the random variable $T_{n,a}$ is a stopping time with respect to the filtration $\mathcal{F}$. +\end{lemma} + +\begin{proof}\leanok +A hitting time of a set by an adapted process is a stopping time. +\end{proof} + + +Let $\Omega' = \mathcal{R}^{\mathbb{N} \times \mathcal{A}}$ and let $\Omega = \Omega_{\mathcal{T}} \times \Omega'$ (which will be an extension of the trajectory probability space once we choose a measure on $\Omega'$). +Let $Z_{n, a} : \Omega \to \mathcal{R}$ be the projection on the coordinate indexed by $(n,a)$ in $\Omega'$. +Extending the probability space in that way allows us to define without ambiguity the reward received when choosing an action for the $n$-th time, even if that action is never actually chosen $n$ times. + + +\begin{definition}[n\textsuperscript{th} reward]\label{def:rewardByCount} + \uses{def:stepsUntil} + \leanok + \lean{Learning.rewardByCount} +We define $Y_{n, a} = R_{T_{n,a}} \mathbb{I}\{T_{n, a} < \infty\} + Z_{n,a} \mathbb{I}\{T_{n, a} = \infty\}$, the reward received when choosing action $a$ for the $n$-th time if that time is finite, and equal to $Z_{n,a}$ otherwise. +In that expression, we see $R_{T_{n,a}}$ and $T_{n, a}$ as random variables on $\Omega$ instead of $\Omega_{\mathcal{T}}$. +\end{definition} + + +\begin{lemma}\label{lem:rewardByCount_pullCount} + \uses{def:rewardByCount, def:pullCount} + \leanok + \lean{Learning.rewardByCount_pullCount_add_one_eq_reward} +$Y_{N_{t, A_t} + 1, A_t} = R_t$. +\end{lemma} + +\begin{proof}\leanok +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. +\end{proof} + + +\section{Scalar rewards} + +TODO: change the name ``reward'' to ``observation'' throughout the chapter? + +We now focus on the case where the reward space is $\mathcal{R} = \mathbb{R}$. + + +\begin{definition}[Sum of rewards]\label{def:sumRewards} + \uses{def: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$. +\end{definition} + + +\begin{definition}[Empirical mean]\label{def:empMean} + \uses{def:sumRewards, def:pullCount} + \leanok + \lean{Learning.empMean} +Let $\hat{\mu}_{t, a} = \frac{S_{t, a}}{N_{t, a}} = \frac{1}{N_{t,a}} \sum_{s=0}^{t-1} R_s \mathbb{I}\{A_s = a\}$ if $N_{t, a} > 0$, and $\hat{\mu}_{t, a} = 0$ otherwise. +This is the empirical mean of the rewards obtained by choosing action $a$ before time $t$. +\end{definition} + +Note: in bandit papers it is common to (implicitly) define the empirical mean as $+\infty$ when the action was never chosen, but in Lean it has to be a real number, and the Lean default value for division by zero is $0$. + + +The following lemma is very useful to relate the two ways of indexing the rewards: by time step and by pull count. + +\begin{lemma}\label{lem:sum_rewardByCount} + \uses{def:rewardByCount, def:pullCount, def:sumRewards} + \leanok + \lean{Learning.sum_rewardByCount_eq_sumRewards} +The sum of the first $N_{t, a}$ rewards received when choosing action $a$ is equal to the sum of the rewards obtained by choosing action $a$ before time $t$: +\begin{align*} + \sum_{n=1}^{N_{t, a}} Y_{n, a} = S_{t,a} + \: . +\end{align*} +\end{lemma} + +\begin{proof}\leanok + +\end{proof} diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 43f4b164..06cff830 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -9,165 +9,109 @@ \section{Algorithm, bandit and probability space} \begin{definition}[Bandit]\label{def:bandit} - \uses{def:environment} + \uses{def:stationaryEnv} \leanok 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. +It is a stationary environment in which the observation space is $\mathcal{R} = \mathbb{R}$. \end{definition} 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}))$. + \item the bandit generates a reward $R_{t+1}$ according to the distribution $\nu(A_{t+1})$, + \item the history is updated to $H_{t+1} = ((A_0, R_0), \ldots, (A_{t+1}, R_{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:algorithm, def:bandit} + \uses{def:algorithm, def:bandit, def:trajMeasure} \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 $\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} - \uses{def:history} - \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}} \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_{1,0}, \ldots, \omega_{1,t})$. + \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. +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_{\mathcal{T}} \times \mathbb{R}^{\mathbb{N} \times \mathcal{A}}$ and $\mathbb{P} = \mathbb{P}_{\mathcal{T}} \otimes (\bigotimes_{n \in \mathbb{N}, a \in \mathcal{A}} \nu(a))$. \end{definition} -\begin{definition}[Pull counts]\label{def:pullCount} - \uses{def:armAndReward} - \leanok - \lean{Learning.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} - +\section{Alternative models: rewards indexed by time or pull count}\label{sec:alt_model} -\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}$. +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. -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}$. +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)$. -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} +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. -\begin{definition}[Filtration]\label{def:banditFiltration} - \uses{def:armAndReward} +\begin{lemma}\label{lem:measurable_comap_indicator_stepsUntil_eq} + \uses{def:stepsUntil} \leanok - \lean{Bandits.filtration} -The filtration $\mathcal{F}_B$ on $\Omega_B$ generated by the history of pulls and rewards is the increasing family of $\sigma$-algebras -$\mathcal{F}_{B,t} = \sigma(H_0, \ldots, H_t)$, for $t \in \mathbb{N}$. -\end{definition} - - -\begin{lemma}\label{lem:adapted_hist} - \uses{def:banditFiltration,def:armAndReward} -Seen as processes defined on $\Omega_B$, the processes $(H_t)_{t \in \mathbb{N}}$, $(A_t)_{t \in \mathbb{N}}$, and $(X_t)_{t \in \mathbb{N}}$ are adapted to the filtration $\mathcal{F}_B$. -\end{lemma} - -\begin{proof} - -\end{proof} - - -\begin{lemma}\label{lem:predictable_pullCount} - \uses{def:banditFiltration,def:pullCount} -Let $a \in \mathcal{A}$. Seen as a process defined on $\Omega_B$, $(N_{t,a})_{t \in \mathbb{N}}$ is predictable with respect to the filtration $\mathcal{F}_B$ (that is, $(N_{t,a})_{t \in \mathbb{N}}$ is adapted to $(\mathcal{F}_{B, t-1})_{t \in \mathbb{N}}$). + \lean{Bandits.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} +\begin{proof}\leanok \end{proof} -\begin{lemma}\label{lem:condDistrib_reward} - \uses{def:Bandit.measure,def:armAndReward} +% todo: move to the previous section about algorithms, in the stationary env section +\begin{lemma}\label{lem:condIndepFun_reward_hist_arm} + \uses{def:actionReward, def:history} \leanok - \lean{Bandits.condDistrib_reward} -The conditional distribution of the reward $X_t$ given the arm $A_t$ in the bandit probability space $(\Omega, \mathbb{P})$ is $\nu(A_t)$. + \lean{Bandits.condIndepFun_reward_hist_arm} +$R_{t+1}$ and $H_t$ are conditionally independent given $A_{t+1}$. \end{lemma} \begin{proof}\leanok - \uses{lem:condDistrib_R_add_one, lem:condDistrib_R_zero} \end{proof} -\begin{lemma}\label{lem:law_arm_zero} - \uses{def:Bandit.measure,def:armAndReward} +\begin{lemma}\label{lem:condIndepFun_reward_stepsUntil_arm} + \uses{def:stepsUntil, def:actionReward, def:Bandit.measure} \leanok - \lean{Bandits.hasLaw_arm_zero} -The law of the arm $A_0$ in the bandit probability space $(\Omega, \mathbb{P})$ is $P_0$. + \lean{Bandits.condIndepFun_reward_stepsUntil_arm} +For $t > 0$, $R_t$ and $\mathbb{I}\{T_{n, a} = t\}$ are conditionally independent given $A_t$. \end{lemma} \begin{proof}\leanok - \uses{lem:law_A_zero} + \uses{lem:measurable_comap_indicator_stepsUntil_eq, lem:condIndepFun_reward_hist_arm} \end{proof} -\begin{lemma}\label{lem:condDistrib_arm} - \uses{def:Bandit.measure,def:armAndReward} +\begin{lemma}\label{lem:reward_cond_stepsUntil} + \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure} \leanok - \lean{Bandits.condDistrib_arm} -The conditional distribution of the arm $A_{t+1}$ given the history $H_t$ in the bandit probability space $(\Omega, \mathbb{P})$ is $\pi_t(H_t)$. + \lean{Bandits.reward_cond_stepsUntil} +Let $n > 0$, $t \in \mathbb{N}$ and suppose that $\mathbb{P}(T_{n, a} = t) > 0$. +Then $P[R_t \mid T_{n, a} = t] = \nu(a)$. \end{lemma} \begin{proof}\leanok - \uses{lem:condDistrib_A_add_one} + \uses{lem:condIndepFun_reward_stepsUntil_arm, lem:condDistrib_reward_stationaryEnv} \end{proof} - -\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. -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:stepsUntil} - \uses{def:pullCount} - \leanok - \lean{Learning.stepsUntil} -For an arm $a \in \mathcal{A}$ and a time $n \in \mathbb{N}$, we denote by $T_{n,a}$ the time at which arm $a$ was pulled for the $n$-th time, that is $T_{n,a} = \min\{s \in \mathbb{N} \mid N_{s+1,a} = n\}$. -Note that $T_{n, a}$ can be infinite if the arm is not pulled $n$ times. -\end{definition} - - -\begin{definition}\label{def:rewardByCount} - \uses{def:stepsUntil} +\begin{lemma}\label{lem:condDistrib_rewardByCount_stepsUntil} + \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure} \leanok - \lean{Learning.rewardByCount} -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} - - -\begin{lemma}\label{lem:isStoppingTime_stepsUntil} - \uses{def:stepsUntil} -$T_{n,a}$ is a stopping time for the filtration generated by the history of pulls and rewards. + \lean{Bandits.condDistrib_rewardByCount_stepsUntil} +For $n > 0$ and $t \in \mathbb{N}$, $P[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} -It is the hitting time of a measurable set by the adapted process $(N_{n+1, a})_{n \in \mathbb{N}}$, hence a stopping time. +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 $P[Y_{n, a} \mid T_{n, a} = t] = P[R_t \mid T_{n, a} = t] = \nu(a)$ by Lemma~\ref{lem:reward_cond_stepsUntil}. + +If $t = \infty$, then $P[Y_{n, a} \mid T_{n, a} = \infty] = P[Z_{n, a} \mid T_{n, a} = \infty]$. By independence of $Z_{n,a}$ and $T_{n, a}$, this is just $\nu(a)$, the law of $Z_{n,a}$. \end{proof} @@ -179,7 +123,7 @@ \section{Alternative model}\label{sec:alt_model} \end{lemma} \begin{proof} - \uses{lem:condDistrib_reward} + \uses{lem:condDistrib_rewardByCount_stepsUntil} It suffices to show that for all $t \in \mathbb{N} \cup \{\infty\}$, the law of $Y_{n,a}$ conditioned on $T_{n,a} = t$ is $\nu(a)$. If $t = \infty$, then \begin{align*} @@ -191,11 +135,11 @@ \section{Alternative model}\label{sec:alt_model} If $t < \infty$, then \begin{align*} \mathcal{L}(Y_{n,a} \mid T_{n,a} = t) - &= \mathcal{L}(X_t \mid T_{n,a} = t) + &= \mathcal{L}(R_t \mid T_{n,a} = t) \\ - &= \mathcal{L}(X_t \mid T_{n,a} = t, A_t = a) + &= \mathcal{L}(R_t \mid T_{n,a} = t, A_t = a) \\ - &= \mathcal{L}(X_t \mid A_t = a) + &= \mathcal{L}(R_t \mid A_t = a) \\ &= \nu(a) \: . @@ -207,12 +151,14 @@ \section{Alternative model}\label{sec:alt_model} \begin{lemma}\label{lem:iIndepFun_rewardByCount} \uses{def:rewardByCount} \leanok - \lean{Bandits.iIndepFun_rewardByCount} + \lean{Bandits.iIndepFun_rewardByCount'} The rewards $(Y_{n,a})_{n \in \mathbb{N}}$ are independent. \end{lemma} \begin{proof} +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})$. +TODO $H_{T_{n,a}}$, $H'_n$ \end{proof} @@ -226,72 +172,44 @@ \section{Alternative model}\label{sec:alt_model} \end{proof} -\begin{lemma}\label{lem:stepsUntil_pullCount_le} - \uses{def:stepsUntil,def:pullCount} - \leanok - \lean{Learning.stepsUntil_pullCount_le} -$T_{N_{t+1, a}, a} \le t < \infty$ for all $t \in \mathbb{N}$ and $a \in \mathcal{A}$. -\end{lemma} - -\begin{proof}\leanok -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} - - -\begin{lemma}\label{lem:stepsUntil_pullCount_eq} - \uses{def:stepsUntil,def:pullCount} - \leanok - \lean{Learning.stepsUntil_pullCount_eq} -$T_{N_{t+1, A_t}, A_t} = t$ for all $t \in \mathbb{N}$. -\end{lemma} - -\begin{proof}\leanok - -\end{proof} - - -\begin{lemma}\label{lem:rewardByCount_pullCount} - \uses{def:rewardByCount,def:pullCount} +\begin{lemma}\label{lem:identDistrib_rewardByCount_stream} + \uses{def:rewardByCount} \leanok - \lean{Learning.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}$. + \lean{Bandits.identDistrib_rewardByCount_stream} +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}\leanok - \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$. + \uses{lem:hasLaw_rewardByCount, lem:iIndepFun_rewardByCount} \end{proof} -\begin{lemma}\label{lem:sum_rewardByCount} - \uses{def:rewardByCount,def:pullCount} +\begin{lemma}\label{lem:identDistrib_sum_Icc_rewardByCount} + \uses{def:rewardByCount} \leanok - \lean{Learning.sum_rewardByCount_eq_sumRewards} -\begin{align*} - \sum_{n=1}^{N_{t, a}} Y_{n, a} = \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\} X_s - \: . -\end{align*} + \lean{Bandits.identDistrib_sum_Icc_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}\leanok - + \uses{lem:identDistrib_rewardByCount_stream} +Immediate consequence of Lemma~\ref{lem:identDistrib_rewardByCount_stream}. \end{proof} - \section{Regret and other bandit quantities} -\begin{definition}\label{def:armMean} +\begin{definition}[Arm means]\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]$. +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)[\mathrm{id}]$. 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, def:armAndReward} + \uses{def:armMean, def:actionReward} \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: @@ -309,6 +227,29 @@ \section{Regret and other bandit quantities} \end{definition} +\begin{lemma}\label{lem:sum_pullCount_mul} + \uses{def:pullCount} + \leanok + \lean{Learning.sum_pullCount_mul} +Let $f : \mathcal{A} \to \mathbb{R}$ be a function on the arms. For all $t \in \mathbb{N}$, +\begin{align*} + \sum_{a \in \mathcal{A}} N_{t,a} f(a) = \sum_{s=0}^{t-1} f(A_s) \: . +\end{align*} +\end{lemma} + +\begin{proof}\leanok +\begin{align*} + \sum_{a \in \mathcal{A}} N_{t,a} f(a) + &= \sum_{a \in \mathcal{A}} \sum_{s=0}^{t-1} \mathbb{I}\{A_s = a\} f(a) + \\ + &= \sum_{s=0}^{t-1} \sum_{a \in \mathcal{A}} \mathbb{I}\{A_s = a\} f(a) + \\ + &= \sum_{s=0}^{t-1} f(A_s) + \: . +\end{align*} +\end{proof} + + \begin{lemma}\label{lem:regret_eq_sum_pullCount_mul_gap} \uses{def:regret,def:gap,def:pullCount} \leanok @@ -319,17 +260,16 @@ \section{Regret and other bandit quantities} \end{align*} \end{lemma} -\begin{proof} - \leanok +\begin{proof}\leanok + \uses{lem:sum_pullCount_mul} +Apply Lemma~\ref{lem:sum_pullCount_mul} with $f(a) = \Delta_a$ to obtain: \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} \Delta_a + &= \sum_{s=0}^{T-1} \Delta_{A_s} \\ - &= \sum_{a \in \mathcal{A}} N_{T,a} \mu^* - \sum_{a \in \mathcal{A}} N_{T,a} \mu_a + &= \sum_{s=0}^{T-1} \mu^* - \sum_{s=0}^{T-1} \mu_{A_s} \\ - &= \sum_{a \in \mathcal{A}} N_{T,a} \Delta_a + &= R_T \: . \end{align*} \end{proof} diff --git a/blueprint/src/chapters/concentration.tex b/blueprint/src/chapters/concentration.tex index 4e59cfef..6ef370c1 100644 --- a/blueprint/src/chapters/concentration.tex +++ b/blueprint/src/chapters/concentration.tex @@ -58,3 +58,24 @@ \chapter{Concentration inequalities} \uses{lem:subGaussian_add_of_indepFun, lem:hoeffding_one} \end{proof} + + +\begin{lemma}\label{lem:measure_sum_le_sum_le'} + \uses{def:subGaussian} + \leanok + \lean{ProbabilityTheory.HasSubgaussianMGF.measure_sum_le_sum_le'} +Let $X_1, \ldots, X_n$ be random variables such that $X_i - P[X_i]$ is $\sigma_{X,i}^2$-sub-Gaussian for $i \in [n]$. +Let $Y_1, \ldots, Y_m$ be random variables such that $Y_i - P[Y_i]$ is $\sigma_{Y,i}^2$-sub-Gaussian for $i \in [m]$. +Suppose further that the vectors $X$ and $Y$ are independent and that $\sum_{i = 1}^m P[Y_i] \le \sum_{i = 1}^n P[X_i]$. +Then +\begin{align*} + \mathbb{P}\left(\sum_{i=1}^m Y_i \ge \sum_{i=1}^n X_i\right) + &\le \exp\left(- \frac{\left(\sum_{i = 1}^n P[X_i] - \sum_{i=1}^m P[Y_i]\right)^2}{2 \sum_{i=1}^n (\sigma_{X,i}^2 + \sigma_{Y,i}^2)}\right) + \: . +\end{align*} +\end{lemma} + +\begin{proof}\leanok + \uses{lem:subGaussian_add_of_indepFun, thm:hoeffding} + +\end{proof} diff --git a/blueprint/src/chapters/etc.tex b/blueprint/src/chapters/etc.tex index daf7dcdf..50e82c48 100644 --- a/blueprint/src/chapters/etc.tex +++ b/blueprint/src/chapters/etc.tex @@ -30,7 +30,19 @@ \section{Explore-Then-Commit} \end{align*} \end{lemma} -\begin{proof} +\begin{proof}\leanok + +\end{proof} + + +\begin{lemma}\label{lem:sumRewards_bestArm_le_of_arm_mul_eq} + \uses{def:etcAlgorithm, def:sumRewards} + \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 \end{proof} @@ -43,30 +55,31 @@ \section{Explore-Then-Commit} Then for the Explore-Then-Commit algorithm with parameter $m$, for any arm $a \in [K]$ with $\Delta_a > 0$, we have $\mathbb{P}(\hat{A}_m^* = a) \le \exp\left(- \frac{m \Delta_a^2}{4}\right)$. \end{lemma} -\begin{proof} - \uses{lem:hasLaw_rewardByCount, lem:iIndepFun_rewardByCount, lem:independent_rewardByCount, lem:sum_rewardByCount, thm:hoeffding} +\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} +By Lemma~\ref{lem:sumRewards_bestArm_le_of_arm_mul_eq}, \begin{align*} \mathbb{P}(\hat{A}_m^* = a) - &\le \mathbb{P}(\hat{\mu}_a \ge \hat{\mu}_{a^*}) - \\ - &= \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) + &\le \mathbb{P}(S_{Km, a} \ge S_{Km, a^*}) \: . \end{align*} -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^*)$. +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}\left(\frac{1}{m} \sum_{i=1}^m Y_{a,i} \ge \frac{1}{m} \sum_{i=1}^m Y_{a^*,i}\right) - \\ - &= \mathbb{P}\left(\frac{1}{m} \sum_{i=1}^m (Y_{a,i} - Y_{a^*,i} + \Delta_a) \ge \Delta_a\right) + \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*} -$Y_{a,i} - Y_{a^*,i} + \Delta_a = (Y_{a,i} - \mu_a) - (Y_{a^*,i} - \mu_{a^*})$ has mean 0 and is 2-sub-Gaussian, since $Y_{a,i}-\mu_a$ and $Y_{a^*,i} - \mu_{a^*}$ are 1-sub-Gaussian and independent. -By Hoeffding's inequality, we have +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 \begin{align*} - \mathbb{P}\left(\frac{1}{m} \sum_{i=1}^m (Y_{a,i} - Y_{a^*,i} + \Delta_a) \ge \Delta_a\right) + \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) + \\ &\le \exp\left(- \frac{m \Delta_a^2}{4}\right) \: . \end{align*} -This concludes the proof. \end{proof} @@ -83,7 +96,7 @@ \section{Explore-Then-Commit} \end{align*} \end{theorem} -\begin{proof} +\begin{proof}\leanok \uses{lem:regret_eq_sum_pullCount_mul_gap, lem:pullCount_etcAlgorithm, lem:prob_etc_error_le_exp} 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$. @@ -93,7 +106,7 @@ \section{Explore-Then-Commit} &\le m + (T - Km) \exp\left(- \frac{m \Delta_a^2}{4}\right) \: . \end{align*} -By definition of the Explore-Then-Commit algorithm (or by Lemma~\ref{lem:pullCount_etcAlgorithm}), +By Lemma~\ref{lem:pullCount_etcAlgorithm}, \begin{align*} N_{T,a} &= m + (T - Km) \mathbb{I}\{\hat{A}_m^* = a\} diff --git a/blueprint/src/chapters/ucb.tex b/blueprint/src/chapters/ucb.tex index e802b863..1cfb5177 100644 --- a/blueprint/src/chapters/ucb.tex +++ b/blueprint/src/chapters/ucb.tex @@ -1 +1,198 @@ \section{UCB} + +\begin{definition}[UCB algorithm]\label{def:ucbAlgorithm} + \uses{def:actionReward, def:pullCount, def:empMean} + \leanok + \lean{Bandits.UCB.nextArm, Bandits.ucbAlgorithm} +The UCB algorithm with parameter $c \in \mathbb{R}_+$ is defined as follows: +\begin{enumerate} + \item for $t < K$, $A_t = t \mod K$ (pull each arm once), + \item for $t \ge K$, $A_t = \arg\max_{a \in [K]} \left( \hat{\mu}_{t,a} + \sqrt{\frac{c \log(t + 1)}{N_{t,a}}} \right)$, where $\hat{\mu}_{t,a} = \frac{1}{N_{t,a}} \sum_{s=0}^{t-1} \mathbb{I}(A_s = a) X_s$ is the empirical mean of the rewards for arm $a$. +\end{enumerate} +\end{definition} + +Note: the argmax in the second step is chosen in a measurable way. + + +\begin{lemma}\label{lem:ucbIndex_le_ucbIndex_arm} + \uses{def:ucbAlgorithm} + \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 +\begin{align*} + \hat{\mu}_{t,a} + \sqrt{\frac{c \log(t + 1)}{N_{t,a}}} + &\le \hat{\mu}_{t,A_t} + \sqrt{\frac{c \log(t + 1)}{N_{t,A_t}}} + \: . +\end{align*} +\end{lemma} + +\begin{proof}\leanok +By definition of the algorithm. +\end{proof} + + +\begin{lemma}\label{lem:gap_arm_le_two_mul_ucbWidth} + \uses{def:ucbAlgorithm} + \leanok + \lean{Bandits.UCB.gap_arm_le_two_mul_ucbWidth, Bandits.UCB.pullCount_arm_le} +Suppose that we have the 3 following conditions: +\begin{enumerate} + \item $\mu^* \le \hat{\mu}_{t, a^*} + \sqrt{\frac{c \log(t + 1)}{N_{t,a^*}}}$, + \item $\hat{\mu}_{t,A_t} - \sqrt{\frac{c \log(t + 1)}{N_{t,A_t}}} \le \mu_{A_t}$, + \item $\hat{\mu}_{t, a^*} + \sqrt{\frac{c \log(t + 1)}{N_{t,a^*}}} \le \hat{\mu}_{t,A_t} + \sqrt{\frac{c \log(t + 1)}{N_{t,A_t}}}$. +\end{enumerate} +Then if $N_{t,A_t} > 0$ we have +\begin{align*} + \Delta_{A_t} + &\le 2 \sqrt{\frac{c \log(t + 1)}{N_{t,A_t}}} + \: . +\end{align*} +And in turn, if $\Delta_{A_t} > 0$ we get +\begin{align*} + N_{t,A_t} + &\le \frac{4 c \log(t + 1)}{\Delta_{A_t}^2} + \: . +\end{align*} + +Note that the third condition is always satisfied for UCB by Lemma~\ref{lem:ucbIndex_le_ucbIndex_arm}, but this lemma, as stated, is independent of the UCB algorithm. +\end{lemma} + +\begin{proof}\leanok + +\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 + \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]$. +Let $c \ge 0$ be a real number. +Then for any time $n \in \mathbb{N}$ and any arm $a \in [K]$, we have +\begin{align*} + P\left(0 < N_{n, a} \ \wedge \ \hat{\mu}_{n, a} + \sqrt{\frac{c \log(n + 1)}{N_{n,a}}} \le \mu_a\right) + &\le \frac{1}{(n + 1)^{c / 2 - 1}} + \: . +\end{align*} +And also, +\begin{align*} + P\left(0 < N_{n, a} \ \wedge \ \hat{\mu}_{n, a} - \sqrt{\frac{c \log(n + 1)}{N_{n,a}}} \ge \mu_a\right) + &\le \frac{1}{(n + 1)^{c / 2 - 1}} + \: . +\end{align*} +\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}$. + +Then apply a union bound over $k \in [1, n]$ and use Lemma~\ref{lem:todo}. +\end{proof} + + +\begin{lemma}\label{lem:pullCount_le_add_three} + \uses{def:pullCount, def:empMean} + \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 +\begin{align*} + N_{n,a} + &\le C + 1 + \\&\quad + + \sum_{s=1}^{n-1} \mathbb{I}\{A_s = a \ \wedge \ C < N_{s,a} \ \wedge \ + \mu^* \le \hat{\mu}_{s, a^*} + \sqrt{\frac{c \log(s + 1)}{N_{s,a^*}}} \ \wedge \ + \hat{\mu}_{s, A_s} - \sqrt{\frac{c \log(s + 1)}{N_{s,A_s}}} \le \mu_{A_s}\} + \\&\quad + + \sum_{s=1}^{n-1} + \mathbb{I}\{0 < N_{s, a^*} \ \wedge \ \hat{\mu}_{s, a^*} + \sqrt{\frac{c \log(s + 1)}{N_{s,a^*}}} < + \mu^*\} + \\&\quad + + \sum_{s=1}^{n-1} + \mathbb{I}\{0 < N_{s, a} \ \wedge \ \mu_a < + \hat{\mu}_{s, a} - \sqrt{\frac{c \log(s + 1)}{N_{s,a}}}\} +\end{align*} +\end{lemma} + +\begin{proof}\leanok + +\end{proof} + + +\begin{lemma}\label{lem:some_sum_eq_zero} + \uses{def:pullCount, def:empMean, def:ucbAlgorithm} + \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} + +\end{proof} + + +\begin{lemma}\label{lem:expectation_pullCount_le} + \uses{def:ucbAlgorithm, def:pullCount, def:empMean} + \leanok + \lean{Bandits.UCB.expectation_pullCount_le} +Suppose that $\nu(a)$ is 1-sub-Gaussian for all arms $a \in [K]$. +For the UCB algorithm with parameter $c > 0$, for any time $n \in \mathbb{N}$ and any arm $a \in [K]$ with positive gap, we have +\begin{align*} + \mathbb{E}[N_{n,a}] + &\le \frac{4 c \log(n + 1)}{\Delta_a^2} + 2 + 2 \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c / 2 - 1}} + \: . +\end{align*} +\end{lemma} + +\begin{proof}\leanok + \uses{lem:pullCount_le_add_three, lem:some_sum_eq_zero, lem:prob_ucbIndex_le} + +\end{proof} + + +\begin{lemma}\label{lem:ucb_regret_le} + \uses{def:ucbAlgorithm, def:regret} + \leanok + \lean{Bandits.UCB.regret_le} +Suppose that $\nu(a)$ is 1-sub-Gaussian for all arms $a \in [K]$. +For the UCB algorithm with parameter $c > 0$, for any time $n \in \mathbb{N}$, we have +\begin{align*} + R_n + &\le \sum_{a : \Delta_a > 0} \left(\frac{4 c \log(n + 1)}{\Delta_a} + 2 \Delta_a\left(1 + \sum_{s=0}^{n-1} \frac{1}{(s + 1)^{c / 2 - 1}}\right)\right) + \: . +\end{align*} +\end{lemma} + +\begin{proof}\leanok + \uses{lem:expectation_pullCount_le, lem:regret_eq_sum_pullCount_mul_gap} + +\end{proof} + +TODO: for $c > 4$, the sum converges to a constant, so we get a logarithmic regret bound. diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 2c69b421..88fb1e0e 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -13,7 +13,6 @@ \input{chapters/etc.tex} \input{chapters/ucb.tex} \input{chapters/practicalAlgorithms.tex} -\input{chapters/sampling.tex} \bibliographystyle{amsalpha} \bibliography{biblio} From fe7831da0b2cb35b91f5e66eef77deb284c501cf Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 1 Jan 2026 13:58:45 +0100 Subject: [PATCH 2/3] more blueprint --- blueprint/lean_decls | 4 +- blueprint/src/chapters/algorithm.tex | 12 ++- blueprint/src/chapters/bandit.tex | 125 ++++++++++++++++++--------- blueprint/src/macros/common.tex | 2 + 4 files changed, 101 insertions(+), 42 deletions(-) diff --git a/blueprint/lean_decls b/blueprint/lean_decls index 8d7621e2..a677429e 100644 --- a/blueprint/lean_decls +++ b/blueprint/lean_decls @@ -45,11 +45,13 @@ Learning.sum_rewardByCount_eq_sumRewards Bandits.Bandit.trajMeasure Bandits.Bandit.measure Bandits.measurable_comap_indicator_stepsUntil_eq -Bandits.condIndepFun_reward_hist_arm +ProbabilityTheory.CondIndepFun.prod_right Bandits.condIndepFun_reward_stepsUntil_arm Bandits.reward_cond_stepsUntil +ProbabilityTheory.condDistrib_ae_eq_cond Bandits.condDistrib_rewardByCount_stepsUntil Bandits.hasLaw_rewardByCount +ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun Bandits.iIndepFun_rewardByCount' Bandits.identDistrib_rewardByCount_stream Bandits.identDistrib_sum_Icc_rewardByCount diff --git a/blueprint/src/chapters/algorithm.tex b/blueprint/src/chapters/algorithm.tex index b91b8835..7b3de6d7 100644 --- a/blueprint/src/chapters/algorithm.tex +++ b/blueprint/src/chapters/algorithm.tex @@ -283,7 +283,7 @@ \section{Stationary environment} \uses{def:actionReward, def:trajMeasure, def:algorithm, def:stationaryEnv} \leanok \lean{Learning.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}$. +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}$). \end{lemma} \begin{proof}\leanok @@ -423,6 +423,16 @@ \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{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} TODO: change the name ``reward'' to ``observation'' throughout the chapter? diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 06cff830..8025229c 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -59,15 +59,13 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al \end{proof} -% todo: move to the previous section about algorithms, in the stationary env section -\begin{lemma}\label{lem:condIndepFun_reward_hist_arm} - \uses{def:actionReward, def:history} +\begin{lemma}\label{lem:CondIndepFun.prod_right} \leanok - \lean{Bandits.condIndepFun_reward_hist_arm} -$R_{t+1}$ and $H_t$ are conditionally independent given $A_{t+1}$. + \lean{ProbabilityTheory.CondIndepFun.prod_right} +If $X \ind Y \mid Z$, then $X \ind (Y, Z) \mid Z$. \end{lemma} -\begin{proof}\leanok +\begin{proof} \end{proof} @@ -76,12 +74,14 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al \uses{def:stepsUntil, def:actionReward, def:Bandit.measure} \leanok \lean{Bandits.condIndepFun_reward_stepsUntil_arm} -For $t > 0$, $R_t$ and $\mathbb{I}\{T_{n, a} = t\}$ are conditionally independent given $A_t$. +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_arm} + \uses{lem:measurable_comap_indicator_stepsUntil_eq, lem:condIndepFun_reward_hist_action, lem:CondIndepFun.prod_right} +$\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}. \end{proof} @@ -89,12 +89,32 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure} \leanok \lean{Bandits.reward_cond_stepsUntil} -Let $n > 0$, $t \in \mathbb{N}$ and suppose that $\mathbb{P}(T_{n, a} = t) > 0$. -Then $P[R_t \mid T_{n, a} = t] = \nu(a)$. +Let $n > 0$, $t \in \mathbb{N}$ and suppose that $P(T_{n, a} = t) > 0$. +Then $\mathcal{L}(R_t \mid T_{n, a} = t) = \nu(a)$. +\end{lemma} + +\begin{proof}\leanok + \uses{lem:stepsUntil_basic, lem:condIndepFun_reward_stepsUntil_arm, 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 +\begin{align*} + \mathcal{L}(R_t \mid T_{n, a} = t, A_t = a) + &= \mathcal{L}(R_t \mid A_t = a) + = \nu(a) + \: . +\end{align*} +\end{proof} + + +\begin{lemma}\label{lem:condDistrib_ae_eq_cond} + \leanok + \lean{ProbabilityTheory.condDistrib_ae_eq_cond} +For a random variable $X$ on a countable space with the discrete sigma algebra, $\mathcal{L}(Y \mid X) = (x \mapsto \mathcal{L}(Y \mid X = x))$, $(X_*P)$-almost surely. +Furthermore, that almost sure equality means that for all $x$ such that $P(X = x) > 0$, we have $\mathcal{L}(Y \mid X = x) = \mathcal{L}(Y \mid X)(x)$. \end{lemma} \begin{proof}\leanok - \uses{lem:condIndepFun_reward_stepsUntil_arm, lem:condDistrib_reward_stationaryEnv} \end{proof} @@ -103,15 +123,16 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al \uses{def:stepsUntil, def:rewardByCount, def:Bandit.measure} \leanok \lean{Bandits.condDistrib_rewardByCount_stepsUntil} -For $n > 0$ and $t \in \mathbb{N}$, $P[Y_{n,a} \mid T_{n,a}] = \nu(a)$ (in which the measure on the r.h.s. is seen as a constant kernel). +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} +\begin{proof}\leanok + \uses{lem:condDistrib_ae_eq_cond, lem:reward_cond_stepsUntil} 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 $P[Y_{n, a} \mid T_{n, a} = t] = P[R_t \mid T_{n, a} = t] = \nu(a)$ by Lemma~\ref{lem:reward_cond_stepsUntil}. +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}. -If $t = \infty$, then $P[Y_{n, a} \mid T_{n, a} = \infty] = P[Z_{n, a} \mid T_{n, a} = \infty]$. By independence of $Z_{n,a}$ and $T_{n, a}$, this is just $\nu(a)$, the law of $Z_{n,a}$. +If $t = \infty$, then $\mathcal{L}(Y_{n, a} \mid T_{n, a} = \infty) = \mathcal{L}(Z_{n, a} \mid T_{n, a} = \infty)$. By independence of $Z_{n,a}$ and $T_{n, a}$, this is just $\nu(a)$, the law of $Z_{n,a}$. \end{proof} @@ -119,32 +140,50 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al \uses{def:rewardByCount} \leanok \lean{Bandits.hasLaw_rewardByCount} -For $n > 0$ and $a \in \mathcal{A}$, the law of $Y_{n,a}$ is $\nu(a)$. +For $n > 0$ and $a \in \mathcal{A}$, $\mathcal{L}(Y_{n,a}) = \nu(a)$. \end{lemma} -\begin{proof} +\begin{proof}\leanok \uses{lem:condDistrib_rewardByCount_stepsUntil} -It suffices to show that for all $t \in \mathbb{N} \cup \{\infty\}$, the law of $Y_{n,a}$ conditioned on $T_{n,a} = t$ is $\nu(a)$. -If $t = \infty$, then -\begin{align*} - \mathcal{L}(Y_{n,a} \mid T_{n,a} = t) - = \mathcal{L}(Z_{n,a} \mid T_{n,a} = t) - = \mathcal{L}(Z_{n,a}) - = \nu(a) -\end{align*} -If $t < \infty$, then -\begin{align*} - \mathcal{L}(Y_{n,a} \mid T_{n,a} = t) - &= \mathcal{L}(R_t \mid T_{n,a} = t) - \\ - &= \mathcal{L}(R_t \mid T_{n,a} = t, A_t = a) - \\ - &= \mathcal{L}(R_t \mid A_t = a) - \\ - &= \nu(a) - \: . -\end{align*} -TODO: explain that chain of equalities. There is independence involved. +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)$. +\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{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} + + +\begin{lemma}\label{lem:indepFun_contraction} +Let $X, Y, Z$ be random variables. If $X \ind Y \mid Z$ and $X \ind Z$, then $X \ind (Y, Z)$. +\end{lemma} + +\begin{proof} +It suffices to show that $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X)$. +By conditional independence, $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X \mid Z)$. +By independence, $\mathcal{L}(X \mid Z) = \mathcal{L}(X)$. +\end{proof} + + +\begin{lemma}\label{lem:iIndepFun_nat_iff_forall_indepFun} + \leanok + \lean{ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun} +A family of random variables $(X_i)_{i \in \mathbb{N}}$ is independent if and only if for all $n \in \mathbb{N}$, $X_{n+1}$ is independent of $(X_0, \ldots, X_n)$. +\end{lemma} + +\begin{proof}\leanok + \end{proof} @@ -156,9 +195,15 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al \end{lemma} \begin{proof} -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})$. + \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}$. + +The fact that $Y_{n+1, a}$ is independent of $T_{n+1, a}$ is Lemma~\ref{lem:indepFun_rewardByCount_stepsUntil}. + +TODO -TODO $H_{T_{n,a}}$, $H'_n$ \end{proof} diff --git a/blueprint/src/macros/common.tex b/blueprint/src/macros/common.tex index e579e1ff..76c6969c 100644 --- a/blueprint/src/macros/common.tex +++ b/blueprint/src/macros/common.tex @@ -17,3 +17,5 @@ \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{remark}[theorem]{Remark} + +\newcommand{\ind}{\perp\!\!\!\!\perp} From 5bd73409b0ece88eaf7527c2ae70a4fe702b6acb Mon Sep 17 00:00:00 2001 From: Remy Degenne Date: Thu, 1 Jan 2026 17:26:54 +0100 Subject: [PATCH 3/3] add appendix --- .../src/appendix/conditional_independence.tex | 45 ++++++++++++++ blueprint/src/chapters/bandit.tex | 60 ++++++++++++------- blueprint/src/content.tex | 4 ++ 3 files changed, 87 insertions(+), 22 deletions(-) create mode 100644 blueprint/src/appendix/conditional_independence.tex diff --git a/blueprint/src/appendix/conditional_independence.tex b/blueprint/src/appendix/conditional_independence.tex new file mode 100644 index 00000000..481dd197 --- /dev/null +++ b/blueprint/src/appendix/conditional_independence.tex @@ -0,0 +1,45 @@ +\chapter{Conditional independence} + + +\begin{lemma}\label{lem:CondIndepFun.prod_right} + \leanok + \lean{ProbabilityTheory.CondIndepFun.prod_right} +If $X \ind Y \mid Z$, then $X \ind (Y, Z) \mid Z$. +\end{lemma} + +\begin{proof} + +\end{proof} + + +\begin{lemma}[Contraction]\label{lem:indepFun_contraction} +If $X \ind Y \mid Z$ and $X \ind Z$, then $X \ind (Y, Z)$. +\end{lemma} + +\begin{proof} +It suffices to show that $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X)$. +By conditional independence, $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X \mid Z)$. +By independence, $\mathcal{L}(X \mid Z) = \mathcal{L}(X)$. +\end{proof} + + +\begin{lemma}\label{lem:condIndepFun_contraction} +If $X \ind Y \mid Z, W$ and $X \ind Z \mid W$, then $X \ind (Y, Z) \mid W$. +\end{lemma} + +\begin{proof} +It suffices to show that $\mathcal{L}(X \mid Y, Z, W) = \mathcal{L}(X \mid W)$. +By the first hypothesis, $\mathcal{L}(X \mid Y, Z, W) = \mathcal{L}(X \mid Z, W)$. +By the second hypothesis, $\mathcal{L}(X \mid Z, W) = \mathcal{L}(X \mid W)$. +\end{proof} + + +\begin{lemma}\label{lem:iIndepFun_nat_iff_forall_indepFun} + \leanok + \lean{ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun} +A family of random variables $(X_i)_{i \in \mathbb{N}}$ is independent if and only if for all $n \in \mathbb{N}$, $X_{n+1}$ is independent of $(X_0, \ldots, X_n)$. +\end{lemma} + +\begin{proof}\leanok + +\end{proof} diff --git a/blueprint/src/chapters/bandit.tex b/blueprint/src/chapters/bandit.tex index 8025229c..a3f3af6a 100644 --- a/blueprint/src/chapters/bandit.tex +++ b/blueprint/src/chapters/bandit.tex @@ -45,6 +45,7 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al With that measure, the law of $Z_{n,a}$ is $\nu(a)$. 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. \begin{lemma}\label{lem:measurable_comap_indicator_stepsUntil_eq} @@ -59,17 +60,6 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al \end{proof} -\begin{lemma}\label{lem:CondIndepFun.prod_right} - \leanok - \lean{ProbabilityTheory.CondIndepFun.prod_right} -If $X \ind Y \mid Z$, then $X \ind (Y, Z) \mid Z$. -\end{lemma} - -\begin{proof} - -\end{proof} - - \begin{lemma}\label{lem:condIndepFun_reward_stepsUntil_arm} \uses{def:stepsUntil, def:actionReward, def:Bandit.measure} \leanok @@ -165,25 +155,51 @@ \section{Alternative models: rewards indexed by time or pull count}\label{sec:al \end{proof} -\begin{lemma}\label{lem:indepFun_contraction} -Let $X, Y, Z$ be random variables. If $X \ind Y \mid Z$ and $X \ind Z$, then $X \ind (Y, Z)$. +\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} -It suffices to show that $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X)$. -By conditional independence, $\mathcal{L}(X \mid Y, Z) = \mathcal{L}(X \mid Z)$. -By independence, $\mathcal{L}(X \mid Z) = \mathcal{L}(X)$. + \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*} + +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} -\begin{lemma}\label{lem:iIndepFun_nat_iff_forall_indepFun} - \leanok - \lean{ProbabilityTheory.iIndepFun_nat_iff_forall_indepFun} -A family of random variables $(X_i)_{i \in \mathbb{N}}$ is independent if and only if for all $n \in \mathbb{N}$, $X_{n+1}$ is independent of $(X_0, \ldots, X_n)$. +\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}\leanok - +\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} diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 88fb1e0e..79e62c88 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -16,3 +16,7 @@ \bibliographystyle{amsalpha} \bibliography{biblio} + +\appendix + +\input{appendix/conditional_independence.tex}