Blueprint: update uses

blueprint/src/chapters/algorithm.tex

@@ -77,7 +77,7 @@ \chapter{Iterative stochastic algorithms}
 
 
 \begin{definition}[Algorithm-environment interaction]\label{def:IsAlgEnvSeq}
-  \uses{def:algorithm, def:environment}
+  \uses{def:environment,def:algorithm,def:history}
   \leanok
   \lean{Learning.IsAlgEnvSeq}
 Let $\mathfrak{A}$ be an algorithm as in Definition~\ref{def:algorithm} and $\mathfrak{E}$ be an environment as in Definition~\ref{def:environment}.
@@ -100,7 +100,7 @@ \chapter{Iterative stochastic algorithms}
 
 
 \begin{lemma}\label{lem:law_step}
-  \uses{def:IsAlgEnvSeq, def:history}
+  \uses{def:environment,def:IsAlgEnvSeq,def:algorithm,def:history}
   \leanok
   \lean{Learning.IsAlgEnvSeq.hasLaw_step_zero, Learning.IsAlgEnvSeq.hasCondDistrib_step}
 In an algorithm-environment interaction $(A, R, P)$ as in Definition~\ref{def:IsAlgEnvSeq},
@@ -116,7 +116,7 @@ \chapter{Iterative stochastic algorithms}
 
 
 \begin{definition}\label{def:IsAlgEnvSeq.filtration}
-  \uses{def:IsAlgEnvSeq, def:history}
+  \uses{def:history}
   \leanok
   \lean{Learning.IsAlgEnvSeq.filtration, Learning.IsAlgEnvSeq.filtrationAction}
 For an algorithm-environment interaction $(A, R, P)$ as in Definition~\ref{def:IsAlgEnvSeq}, we denote by $\mathcal{F}_t$ the sigma-algebra generated by the history up to time $t$: $\mathcal{F}_t = \sigma(H_t)$.
@@ -125,13 +125,14 @@ \chapter{Iterative stochastic algorithms}
 
 
 \begin{theorem}[\cite{lattimore2020bandit}, Proposition 4.8]\label{thm:isAlgEnvSeq_unique}
-  \uses{def:IsAlgEnvSeq}
+  \uses{def:environment,def:IsAlgEnvSeq,def:algorithm}
   \leanok
   \lean{Learning.isAlgEnvSeq_unique}
 If $(A, R, P)$ and $(A', R', P')$ are two algorithm-environment interactions for the same algorithm $\mathfrak{A}$ and environment $\mathfrak{E}$, then the joint distributions of the sequences of actions and observations are equal: the law of $(A_i, R_i)_{i \in \mathbb{N}}$ under $P$ is equal to the law of $(A'_i, R'_i)_{i \in \mathbb{N}}$ under $P'$.
 \end{theorem}
 
 \begin{proof}\leanok
+  \uses{thm:ionescu-tulcea,lem:law_step,def:trajMeasure}
 
 \end{proof}
 
@@ -144,20 +145,20 @@ \section{Stationary environment}
 Let $(A, R, P)$ be an algorithm-environment interaction in a stationary environment with kernel $\nu$.
 
 \begin{lemma}\label{lem:condDistrib_reward_stationaryEnv}
-  \uses{def:IsAlgEnvSeq, def:stationaryEnv}
+  \uses{def:stationaryEnv,def:IsAlgEnvSeq,def:algorithm}
   \leanok
   \lean{Learning.IsAlgEnvSeq.condDistrib_reward_stationaryEnv}
 In a stationary environment, for any $t \in \mathbb{N}$, the conditional distribution $P\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:law_step, def:stationaryEnv}
+  \uses{def:environment,lem:law_step,def:history}
 
 \end{proof}
 
 
 \begin{lemma}\label{lem:condIndepFun_reward_hist_action}
-  \uses{def:IsAlgEnvSeq, def:stationaryEnv}
+  \uses{def:stationaryEnv,def:environment,def:IsAlgEnvSeq,def:algorithm,def:history}
   \leanok
   \lean{Learning.IsAlgEnvSeq.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}$ (more succinctly, $R_{t+1} \ind H_t \mid A_{t+1}$).
@@ -244,7 +245,7 @@ \subsection{Ionescu-Tulcea theorem}
 
 
 \begin{lemma}\label{lem:IT.condDistrib_X_add_one}
-  \uses{def:IT.history, def:trajMeasure}
+  \uses{def:IT.history, thm:ionescu-tulcea, def:trajMeasure}
   \leanok
   \lean{ProbabilityTheory.Kernel.condDistrib_trajMeasure}
 For any $t \in \mathbb{N}$, the conditional distribution $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right]$ is $((H_t)_* P_{\mathcal{T}})$-almost surely equal to $\kappa_t$.
@@ -304,28 +305,28 @@ \subsection{Case of an algorithm-environment interaction}
 We need to check that the random variables $A_t$ and $R_t$ have the expected conditional distributions.
 
 \begin{lemma}\label{lem:IT.condDistrib_A_add_one}
-  \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment}
+  \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure,def:IT.history}
   \leanok
   \lean{Learning.IT.condDistrib_action}
 For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left[A_{t+1} \mid H_t\right] = \pi_t$.
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:IT.condDistrib_X_add_one}
+  \uses{lem:IT.condDistrib_X_add_one,def:IT.history}
 By Lemma~\ref{lem:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right] = \kappa_t = \pi_t \otimes \nu_t$.
 Since $A_{t+1}$ is the projection of $X_{t+1}$ on $\mathcal{A}$, $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}$, which is $\pi_t$.
 \end{proof}
 
 
 \begin{lemma}\label{lem:IT.condDistrib_R_add_one}
-  \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment}
+  \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure,def:IT.history}
   \leanok
   \lean{Learning.IT.condDistrib_reward}
 For any $t \in \mathbb{N}$, $P_{\mathcal{T}}\left[R_{t+1} \mid H_t, A_{t+1}\right] = \nu_t$.
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:IT.condDistrib_X_add_one, lem:IT.condDistrib_A_add_one}
+  \uses{lem:IT.condDistrib_X_add_one,def:IT.history,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:IT.condDistrib_X_add_one}, $P_{\mathcal{T}}\left[X_{t+1} \mid H_t\right] = \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}}$.
@@ -337,27 +338,27 @@ \subsection{Case of an algorithm-environment interaction}
 
 
 \begin{lemma}\label{lem:IT.law_A_zero}
-  \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment}
+  \uses{def:environment,def:algorithm,def:IT.actionReward,def:trajMeasure}
   \leanok
   \lean{Learning.IT.hasLaw_action_zero}
 The law of $A_0$ under $P_{\mathcal{T}}$ is $P_0$.
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:IT.law_X_zero}
+  \uses{thm:ionescu-tulcea,def:IT.history,lem:IT.law_X_zero}
 $X_0$ has law $\mu = P_0 \otimes \nu'_0$. $A_0$ is the projection of $X_0$ on the first space $\mathcal{A}$ and $\nu_0'$ is Markov, so $A_0$ has law $P_0$.
 \end{proof}
 
 
 \begin{lemma}\label{lem:IT.condDistrib_R_zero}
-  \uses{def:IT.actionReward, def:trajMeasure, def:algorithm, def:environment}
+  \uses{def:environment,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure}
   \leanok
   \lean{Learning.IT.condDistrib_reward_zero}
 $P_{\mathcal{T}}\left[R_0 \mid A_0\right] = \nu'_0$.
 \end{lemma}
 
 \begin{proof}\leanok
-  \uses{lem:IT.law_X_zero}
+  \uses{lem:IT.law_X_zero,lem:IT.law_A_zero,def:IT.history}
 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:IT.law_X_zero}, $X_{0*} P_{\mathcal{T}} = \mu = P_0 \otimes \nu'_0$.
@@ -367,14 +368,14 @@ \subsection{Case of an algorithm-environment interaction}
 
 
 \begin{theorem}\label{thm:isAlgEnvSeq_trajMeasure}
-  \uses{def:IsAlgEnvSeq, def:trajMeasure}
+  \uses{def:environment,def:IsAlgEnvSeq,def:algorithm,thm:ionescu-tulcea,def:IT.actionReward,def:trajMeasure}
   \leanok
   \lean{Learning.IT.isAlgEnvSeq_trajMeasure}
 In the probability space $(\Omega_{\mathcal{T}}, P_{\mathcal{T}})$ constructed from an algorithm $\mathfrak{A}$ and an environment $\mathfrak{E}$ as above, the sequences of random variables $A : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{A}$ and $R : \mathbb{N} \to \Omega_{\mathcal{T}} \to \mathcal{R}$ form an algorithm-environment interaction for $\mathfrak{A}$ and $\mathfrak{E}$.
 \end{theorem}
 
 \begin{proof}\leanok
-  \uses{lem:IT.law_A_zero, lem:IT.condDistrib_R_zero, lem:IT.condDistrib_A_add_one, lem:IT.condDistrib_R_add_one}
+  \uses{def:history,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}
 
@@ -386,7 +387,6 @@ \section{Finitely many actions}
 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:IT.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\}$.
@@ -434,6 +434,7 @@ \section{Finitely many actions}
 \end{lemma}
 
 \begin{proof}\leanok
+  \uses{def:history,lem:pullCount_basic}
 
 \end{proof}
 
@@ -467,6 +468,7 @@ \section{Finitely many actions}
 \end{lemma}
 
 \begin{proof}\leanok
+  \uses{lem:pullCount_basic,def:pullCount}
 
 \end{proof}
 
@@ -479,6 +481,7 @@ \section{Finitely many actions}
 \end{lemma}
 
 \begin{proof}\leanok
+  \uses{def:history,lem:pullCount_basic,def:pullCount}
 A hitting time of a set by an adapted process is a stopping time.
 \end{proof}
 
@@ -505,6 +508,7 @@ \section{Finitely many actions}
 \end{lemma}
 
 \begin{proof}\leanok
+  \uses{lem:stepsUntil_basic,def:stepsUntil}
 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.
@@ -529,7 +533,6 @@ \section{Scalar rewards}
 
 
 \begin{definition}[Sum of rewards]\label{def:sumRewards}
-  \uses{def:IT.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$.
@@ -561,5 +564,6 @@ \section{Scalar rewards}
 \end{lemma}
 
 \begin{proof}\leanok
+  \uses{lem:rewardByCount_pullCount}
 
 \end{proof}